Metamath Proof Explorer


Theorem 19.21a3con13vVD

Description: Virtual deduction proof of alrim3con13v . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1:: |- (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
2:: |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
3:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2 |- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
11:10:in2 |- (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
qed:11:in1 |- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.21a3con13vVD φxφψφχxψφχ

Proof

Step Hyp Ref Expression
1 idn2 φxφ,ψφχψφχ
2 simp1 ψφχψ
3 1 2 e2 φxφ,ψφχψ
4 ax-5 ψxψ
5 3 4 e2 φxφ,ψφχxψ
6 idn1 φxφφxφ
7 simp2 ψφχφ
8 1 7 e2 φxφ,ψφχφ
9 id φxφφxφ
10 6 8 9 e12 φxφ,ψφχxφ
11 simp3 ψφχχ
12 1 11 e2 φxφ,ψφχχ
13 ax-5 χxχ
14 12 13 e2 φxφ,ψφχxχ
15 pm3.2an3 xψxφxχxψxφxχ
16 5 10 14 15 e222 φxφ,ψφχxψxφxχ
17 19.26-3an xψφχxψxφxχ
18 17 biimpri xψxφxχxψφχ
19 16 18 e2 φxφ,ψφχxψφχ
20 19 in2 φxφψφχxψφχ
21 20 in1 φxφψφχxψφχ