Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  19.41rgVD Unicode version

Theorem 19.41rgVD 28994
Description: Virtual deduction proof of 19.41rg 28615. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 19.41rg 28615 is 19.41rgVD 28994 without virtual deductions and was automatically derived from 19.41rgVD 28994. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  ( ps  ->  ( ph  ->  ( ph  /\  ps ) ) )
2:1:  |-  ( ( ps  ->  A. x ps )  ->  ( ps  ->  ( ph  ->  (  ph  /\  ps ) ) ) )
3:2:  |-  A. x ( ( ps  ->  A. x ps )  ->  ( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
4:3:  |-  ( A. x ( ps  ->  A. x ps )  ->  ( A. x ps  ->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
5::  |-  (. A. x ( ps  ->  A. x ps )  ->.  A. x ( ps  ->  A. x ps ) ).
6:4,5:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x ( ph  ->  ( ph  /\  ps ) ) ) ).
7::  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  A. x ps ).
8:6,7:  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  A. x ( ph  ->  ( ph  /\  ps ) ) ).
9:8:  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  ( E. x ph  ->  E. x ( ph  /\  ps ) ) ).
10:9:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x ( ph  /\  ps ) ) ) ).
11:5:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  A.  x ps ) ).
12:10,11:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  (  E. x ph  ->  E. x ( ph  /\  ps ) ) ) ).
13:12:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\  ps ) ) ) ).
14:13:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x  ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) ).
qed:14:  |-  ( A. x ( ps  ->  A. x ps )  ->  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) )
Assertion
Ref Expression
19.41rgVD  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ( E. x ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) )

Proof of Theorem 19.41rgVD
StepHypRef Expression
1 idn1 28641 . . . . . . . . 9  |-  (. A. x ( ps  ->  A. x ps )  ->.  A. x
( ps  ->  A. x ps ) ).
2 pm3.2 434 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
32com12 27 . . . . . . . . . . . 12  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
43a1i 10 . . . . . . . . . . 11  |-  ( ( ps  ->  A. x ps )  ->  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) ) )
54ax-gen 1536 . . . . . . . . . 10  |-  A. x
( ( ps  ->  A. x ps )  -> 
( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
6 3ax5 28599 . . . . . . . . . 10  |-  ( A. x ( ( ps 
->  A. x ps )  ->  ( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )  ->  ( A. x
( ps  ->  A. x ps )  ->  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) ) )
75, 6e0_ 28861 . . . . . . . . 9  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x ps 
->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
81, 7e1_ 28704 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) ).
9 idn2 28690 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x ps ).
10 id 19 . . . . . . . 8  |-  ( ( A. x ps  ->  A. x ( ph  ->  (
ph  /\  ps )
) )  ->  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) )
118, 9, 10e12 28813 . . . . . . 7  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x
( ph  ->  ( ph  /\ 
ps ) ) ).
12 exim 1565 . . . . . . 7  |-  ( A. x ( ph  ->  (
ph  /\  ps )
)  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )
1311, 12e2 28708 . . . . . 6  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  ( E. x ph  ->  E. x
( ph  /\  ps )
) ).
1413in2 28682 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) ) ).
15 sp 1728 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
161, 15e1_ 28704 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  A. x ps ) ).
17 imim2 49 . . . . 5  |-  ( ( A. x ps  ->  ( E. x ph  ->  E. x ( ph  /\  ps ) ) )  -> 
( ( ps  ->  A. x ps )  -> 
( ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) ) ) )
1814, 16, 17e11 28765 . . . 4  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) ) ).
19 pm2.04 76 . . . 4  |-  ( ( ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )  ->  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) )
2018, 19e1_ 28704 . . 3  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) ).
21 pm3.31 432 . . 3  |-  ( ( E. x ph  ->  ( ps  ->  E. x
( ph  /\  ps )
) )  ->  (
( E. x ph  /\ 
ps )  ->  E. x
( ph  /\  ps )
) )
2220, 21e1_ 28704 . 2  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\ 
ps ) ) ).
2322in1 28638 1  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ( E. x ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1530   E.wex 1531
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-vd1 28637  df-vd2 28646
  Copyright terms: Public domain W3C validator