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

Theorem hbimpgVD 28680
Description: Virtual deduction proof of hbimpg 28320. 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 28320 is hbimpgVD 28680 without virtual deductions and was automatically derived from hbimpgVD 28680. (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 1719 . . . 4  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (
ph  ->  A. x ph )
)
2 hba1 1719 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x ( ps  ->  A. x ps ) )
31, 2hban 1736 . . 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 28385 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  -.  ph ).
5 idn1 28342 . . . . . . . . . . 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_ 28399 . . . . . . . . . 10  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
8 hbntal 28319 . . . . . . . . . 10  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
97, 8e1_ 28399 . . . . . . . . 9  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
10 sp 1716 . . . . . . . . 9  |-  ( A. x ( -.  ph  ->  A. x  -.  ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
119, 10e1_ 28399 . . . . . . . 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 28505 . . . . . . 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 1546 . . . . . . 7  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  ps )
)
1613, 15e2 28403 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x
( ph  ->  ps ) ).
1716in2 28377 . . . . 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_ 28399 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
20 sp 1716 . . . . . . 7  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
2119, 20e1_ 28399 . . . . . 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 1546 . . . . . 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 28467 . . . . 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 28460 . . . 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 28467 . . 3  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
323, 31gen11nv 28389 . 2  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
3332in1 28339 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 1527
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-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-vd1 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator