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

Theorem 19.41rgVD 34103
Description: Virtual deduction proof of 19.41rg 33717. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 19.41rg 33717 is 19.41rgVD 34103 without virtual deductions and was automatically derived from 19.41rgVD 34103. (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 33745 . . . . . . . . 9  |-  (. A. x ( ps  ->  A. x ps )  ->.  A. x
( ps  ->  A. x ps ) ).
2 pm3.2 445 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
32com12 31 . . . . . . . . . . . 12  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
43a1i 11 . . . . . . . . . . 11  |-  ( ( ps  ->  A. x ps )  ->  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) ) )
54ax-gen 1623 . . . . . . . . . 10  |-  A. x
( ( ps  ->  A. x ps )  -> 
( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
6 al2im 1640 . . . . . . . . . 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, 6e0a 33963 . . . . . . . . 9  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x ps 
->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
81, 7e1a 33807 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) ).
9 idn2 33793 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x ps ).
10 id 22 . . . . . . . 8  |-  ( ( A. x ps  ->  A. x ( ph  ->  (
ph  /\  ps )
) )  ->  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) )
118, 9, 10e12 33915 . . . . . . 7  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x
( ph  ->  ( ph  /\ 
ps ) ) ).
12 exim 1659 . . . . . . 7  |-  ( A. x ( ph  ->  (
ph  /\  ps )
)  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )
1311, 12e2 33811 . . . . . 6  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  ( E. x ph  ->  E. x
( ph  /\  ps )
) ).
1413in2 33785 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) ) ).
15 sp 1864 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
161, 15e1a 33807 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  A. x ps ) ).
17 imim2 53 . . . . 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 33868 . . . 4  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) ) ).
19 pm2.04 82 . . . 4  |-  ( ( ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )  ->  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) )
2018, 19e1a 33807 . . 3  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) ).
21 pm3.31 443 . . 3  |-  ( ( E. x ph  ->  ( ps  ->  E. x
( ph  /\  ps )
) )  ->  (
( E. x ph  /\ 
ps )  ->  E. x
( ph  /\  ps )
) )
2220, 21e1a 33807 . 2  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\ 
ps ) ) ).
2322in1 33742 1  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ( E. x ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1396   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-vd1 33741  df-vd2 33749
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator