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 
|- ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 idn2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( ps /\ ph /\ ch ) ).
2 simp1 
 |-  ( ( ps /\ ph /\ ch ) -> ps )
3 1 2 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4 ax-5 
 |-  ( ps -> A. x ps )
5 3 4 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
6 idn1 
 |-  (. ( ph -> A. x ph ) ->. ( ph -> A. x ph ) ).
7 simp2 
 |-  ( ( ps /\ ph /\ ch ) -> ph )
8 1 7 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
9 id 
 |-  ( ( ph -> A. x ph ) -> ( ph -> A. x ph ) )
10 6 8 9 e12 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
11 simp3 
 |-  ( ( ps /\ ph /\ ch ) -> ch )
12 1 11 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
13 ax-5 
 |-  ( ch -> A. x ch )
14 12 13 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
15 pm3.2an3 
 |-  ( A. x ps -> ( A. x ph -> ( A. x ch -> ( A. x ps /\ A. x ph /\ A. x ch ) ) ) )
16 5 10 14 15 e222 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
17 19.26-3an 
 |-  ( A. x ( ps /\ ph /\ ch ) <-> ( A. x ps /\ A. x ph /\ A. x ch ) )
18 17 biimpri 
 |-  ( ( A. x ps /\ A. x ph /\ A. x ch ) -> A. x ( ps /\ ph /\ ch ) )
19 16 18 e2 
 |-  (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ( ps /\ ph /\ ch ) ).
20 19 in2 
 |-  (. ( ph -> A. x ph ) ->. ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) ).
21 20 in1 
 |-  ( ( ph -> A. x ph ) -> ( ( ps /\ ph /\ ch ) -> A. x ( ps /\ ph /\ ch ) ) )