Theorem rexim1 ≪ | index | src | ≫

theorem rexim1 (b: wff) {x: nat} (a c: wff x):
  $ E. x (a /\ (b -> c)) -> b -> E. x (a /\ c) $;

Step	Hyp	Ref	Expression
1		mpcom	b -> (b -> c) -> c
2	1	anim2d	b -> a /\ (b -> c) -> a /\ c
3	2	eximd	b -> E. x (a /\ (b -> c)) -> E. x (a /\ c)
4	3	com12	E. x (a /\ (b -> c)) -> 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)