Theorem ralan | index | src |

theorem ralan {x: nat} (a b c: wff x):
  $ A. x (a -> b /\ c) <-> A. x (a -> b) /\ A. x (a -> c) $;
StepHypRefExpression
1 bitr
(A. x (a -> b /\ c) <-> A. x ((a -> b) /\ (a -> c))) ->
  (A. x ((a -> b) /\ (a -> c)) <-> A. x (a -> b) /\ A. x (a -> c)) ->
  (A. x (a -> b /\ c) <-> A. x (a -> b) /\ A. x (a -> c))
2 imandi
a -> b /\ c <-> (a -> b) /\ (a -> c)
3 2 aleqi
A. x (a -> b /\ c) <-> A. x ((a -> b) /\ (a -> c))
4 1, 3 ax_mp
(A. x ((a -> b) /\ (a -> c)) <-> A. x (a -> b) /\ A. x (a -> c)) -> (A. x (a -> b /\ c) <-> A. x (a -> b) /\ A. x (a -> c))
5 alan
A. x ((a -> b) /\ (a -> c)) <-> A. x (a -> b) /\ A. x (a -> c)
6 4, 5 ax_mp
A. x (a -> b /\ c) <-> A. x (a -> b) /\ A. x (a -> c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4)