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 29015
Description: Virtual deduction proof of 19.41rg 28638. 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 28638 is 19.41rgVD 29015 without virtual deductions and was automatically derived from 19.41rgVD 29015. (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 28666 . . . . . . . . 9  |-  (. A. x ( ps  ->  A. x ps )  ->.  A. x
( ps  ->  A. x ps ) ).
2 pm3.2 436 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
32com12 30 . . . . . . . . . . . 12  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
43a1i 11 . . . . . . . . . . 11  |-  ( ( ps  ->  A. x ps )  ->  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) ) )
54ax-gen 1556 . . . . . . . . . 10  |-  A. x
( ( ps  ->  A. x ps )  -> 
( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
6 3ax5 28622 . . . . . . . . . 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_ 28885 . . . . . . . . 9  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x ps 
->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
81, 7e1_ 28729 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) ).
9 idn2 28715 . . . . . . . 8  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x ps ).
10 id 21 . . . . . . . 8  |-  ( ( A. x ps  ->  A. x ( ph  ->  (
ph  /\  ps )
) )  ->  ( A. x ps  ->  A. x
( ph  ->  ( ph  /\ 
ps ) ) ) )
118, 9, 10e12 28837 . . . . . . 7  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  A. x
( ph  ->  ( ph  /\ 
ps ) ) ).
12 exim 1585 . . . . . . 7  |-  ( A. x ( ph  ->  (
ph  /\  ps )
)  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )
1311, 12e2 28733 . . . . . 6  |-  (. A. x ( ps  ->  A. x ps ) ,.
A. x ps  ->.  ( E. x ph  ->  E. x
( ph  /\  ps )
) ).
1413in2 28707 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) ) ).
15 sp 1764 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
161, 15e1_ 28729 . . . . 5  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  A. x ps ) ).
17 imim2 52 . . . . 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 28790 . . . 4  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) ) ).
19 pm2.04 79 . . . 4  |-  ( ( ps  ->  ( E. x ph  ->  E. x
( ph  /\  ps )
) )  ->  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) )
2018, 19e1_ 28729 . . 3  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\ 
ps ) ) ) ).
21 pm3.31 434 . . 3  |-  ( ( E. x ph  ->  ( ps  ->  E. x
( ph  /\  ps )
) )  ->  (
( E. x ph  /\ 
ps )  ->  E. x
( ph  /\  ps )
) )
2220, 21e1_ 28729 . 2  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\ 
ps ) ) ).
2322in1 28663 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 360   A.wal 1550   E.wex 1551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-vd1 28662  df-vd2 28671
  Copyright terms: Public domain W3C validator