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

Theorem 19.41rgVD 28678
Description: Virtual deduction proof of 19.41rg 28316. 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 28316 is 19.41rgVD 28678 without virtual deductions and was automatically derived from 19.41rgVD 28678. (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 28342 . . . . . . . . 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 1533 . . . . . . . . . 10  |-  A. x
( ( ps  ->  A. x ps )  -> 
( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
6 3ax5 28300 . . . . . . . . . 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_ 28547 . . . . . . . . 9  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x ps 
->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
81, 7e1_ 28399 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) ).
9 idn2 28385 . . . . . . . 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 28499 . . . . . . 7  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x
( ph  ->  ( ph  /\ 
ps ) ) ).
12 exim 1562 . . . . . . 7  |-  ( A. x ( ph  ->  (
ph  /\  ps )
)  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )
1311, 12e2 28403 . . . . . 6  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  ( E. x ph  ->  E. x
( ph  /\  ps )
) ).
1413in2 28377 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) ) ).
15 sp 1716 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
161, 15e1_ 28399 . . . . 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 28460 . . . 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_ 28399 . . 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_ 28399 . 2  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\ 
ps ) ) ).
2322in1 28339 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 1527   E.wex 1528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-vd1 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator