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

Theorem hbimpgVD 28444
Description: Virtual deduction proof of hbimpg 28067. 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. hbimpg 28067 is hbimpgVD 28444 without virtual deductions and was automatically derived from hbimpgVD 28444. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ).
2:1:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
3::  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  -.  ph ).
4:2:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x -.  ph ) ).
5:4:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x -.  ph ) ).
6:3,5:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  A. x -.  ph ).
7::  |-  ( -.  ph  ->  ( ph  ->  ps ) )
8:7:  |-  ( A. x -.  ph  ->  A. x ( ph  ->  ps ) )
9:6,8:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  A. x ( ph  ->  ps ) ).
10:9:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x ( ph  ->  ps ) ) ).
11::  |-  ( ps  ->  ( ph  ->  ps ) )
12:11:  |-  ( A. x ps  ->  A. x ( ph  ->  ps ) )
13:1:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
14:13:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ps ) ).
15:14,12:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ( ph  ->  ps ) ) ).
16:10,15:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ).
17::  |-  ( ( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
18:16,17:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ).
19::  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (  ph  ->  A. x ph ) )
20::  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x (  ps  ->  A. x ps ) )
21:19,20:  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->  A. x ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) )
22:21,18:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ).
qed:22:  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->  A. x ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) )
Assertion
Ref Expression
hbimpgVD  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) )

Proof of Theorem hbimpgVD
StepHypRef Expression
1 hba1 1792 . . . 4  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (
ph  ->  A. x ph )
)
2 hba1 1792 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x ( ps  ->  A. x ps ) )
31, 2hban 1838 . . 3  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( A. x (
ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
) )
4 idn2 28138 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  -.  ph ).
5 idn1 28089 . . . . . . . . . . 11  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
) ).
6 simpl 443 . . . . . . . . . . 11  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ph  ->  A. x ph ) )
75, 6e1_ 28152 . . . . . . . . . 10  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
8 hbntal 28066 . . . . . . . . . 10  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
97, 8e1_ 28152 . . . . . . . . 9  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
10 sp 1753 . . . . . . . . 9  |-  ( A. x ( -.  ph  ->  A. x  -.  ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
119, 10e1_ 28152 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x  -.  ph ) ).
12 pm2.27 35 . . . . . . . 8  |-  ( -. 
ph  ->  ( ( -. 
ph  ->  A. x  -.  ph )  ->  A. x  -.  ph ) )
134, 11, 12e21 28267 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x  -.  ph ).
14 pm2.21 100 . . . . . . . 8  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
1514alimi 1564 . . . . . . 7  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  ps )
)
1613, 15e2 28156 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x
( ph  ->  ps ) ).
1716in2 28130 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x
( ph  ->  ps )
) ).
18 simpr 447 . . . . . . . 8  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ps  ->  A. x ps ) )
195, 18e1_ 28152 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
20 sp 1753 . . . . . . 7  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
2119, 20e1_ 28152 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ps ) ).
22 ax-1 5 . . . . . . 7  |-  ( ps 
->  ( ph  ->  ps ) )
2322alimi 1564 . . . . . 6  |-  ( A. x ps  ->  A. x
( ph  ->  ps )
)
24 imim1 70 . . . . . 6  |-  ( ( ps  ->  A. x ps )  ->  ( ( A. x ps  ->  A. x ( ph  ->  ps ) )  ->  ( ps  ->  A. x ( ph  ->  ps ) ) ) )
2521, 23, 24e10 28220 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x
( ph  ->  ps )
) ).
26 jao 498 . . . . 5  |-  ( ( -.  ph  ->  A. x
( ph  ->  ps )
)  ->  ( ( ps  ->  A. x ( ph  ->  ps ) )  -> 
( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ) )
2717, 25, 26e11 28213 . . . 4  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ).
28 imor 401 . . . 4  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
29 imbi1 313 . . . . 5  |-  ( ( ( ph  ->  ps ) 
<->  ( -.  ph  \/  ps ) )  ->  (
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
)  <->  ( ( -. 
ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3029biimprcd 216 . . . 4  |-  ( ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
)  ->  ( (
( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )  ->  (
( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3127, 28, 30e10 28220 . . 3  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
323, 31gen11nv 28142 . 2  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
3332in1 28086 1  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1545
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1547  df-nf 1550  df-vd1 28085  df-vd2 28094
  Copyright terms: Public domain W3C validator