Theorem rexpim1 | index | src |

theorem rexpim1 {x y: nat} (a: wff x) (b: wff y) (c: wff x y):
  $ E. x (a /\ (P. y b -> c)) -> (P. y b -> E. x (a /\ c)) $;
StepHypRefExpression
1 anrl
a /\ (E. y b /\ A. y (b -> c)) -> E. y b
2 1 conv pim
a /\ (P. y b -> c) -> E. y b
3 2 eex
E. x (a /\ (P. y b -> c)) -> E. y b
4 anim2
((P. y b -> c) -> A. y (b -> c)) -> a /\ (P. y b -> c) -> a /\ A. y (b -> c)
5 anr
E. y b /\ A. y (b -> c) -> A. y (b -> c)
6 5 conv pim
(P. y b -> c) -> A. y (b -> c)
7 4, 6 ax_mp
a /\ (P. y b -> c) -> a /\ A. y (b -> c)
8 7 eximi
E. x (a /\ (P. y b -> c)) -> E. x (a /\ A. y (b -> c))
9 rexral
E. x (a /\ A. y (b -> c)) -> A. y (b -> E. x (a /\ c))
10 8, 9 rsyl
E. x (a /\ (P. y b -> c)) -> A. y (b -> E. x (a /\ c))
11 3, 10 iand
E. x (a /\ (P. y b -> c)) -> E. y b /\ A. y (b -> E. x (a /\ c))
12 11 conv pim
E. x (a /\ (P. y b -> c)) -> (P. y b -> E. x (a /\ c))

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12)