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

Theorem hbimpgVD 34105
Description: Virtual deduction proof of hbimpg 33721. 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. hbimpg 33721 is hbimpgVD 34105 without virtual deductions and was automatically derived from hbimpgVD 34105. (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 1901 . . . 4  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (
ph  ->  A. x ph )
)
2 hba1 1901 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x ( ps  ->  A. x ps ) )
31, 2hban 1936 . . 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 33793 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  -.  ph ).
5 idn1 33745 . . . . . . . . . . 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 455 . . . . . . . . . . 11  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ph  ->  A. x ph ) )
75, 6e1a 33807 . . . . . . . . . 10  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
8 hbntal 33720 . . . . . . . . . 10  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
97, 8e1a 33807 . . . . . . . . 9  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
10 sp 1864 . . . . . . . . 9  |-  ( A. x ( -.  ph  ->  A. x  -.  ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
119, 10e1a 33807 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x  -.  ph ) ).
12 pm2.27 39 . . . . . . . 8  |-  ( -. 
ph  ->  ( ( -. 
ph  ->  A. x  -.  ph )  ->  A. x  -.  ph ) )
134, 11, 12e21 33921 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x  -.  ph ).
14 pm2.21 108 . . . . . . . 8  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
1514alimi 1638 . . . . . . 7  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  ps )
)
1613, 15e2 33811 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x
( ph  ->  ps ) ).
1716in2 33785 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x
( ph  ->  ps )
) ).
18 simpr 459 . . . . . . . 8  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ps  ->  A. x ps ) )
195, 18e1a 33807 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
20 sp 1864 . . . . . . 7  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
2119, 20e1a 33807 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ps ) ).
22 ax-1 6 . . . . . . 7  |-  ( ps 
->  ( ph  ->  ps ) )
2322alimi 1638 . . . . . 6  |-  ( A. x ps  ->  A. x
( ph  ->  ps )
)
24 imim1 76 . . . . . 6  |-  ( ( ps  ->  A. x ps )  ->  ( ( A. x ps  ->  A. x ( ph  ->  ps ) )  ->  ( ps  ->  A. x ( ph  ->  ps ) ) ) )
2521, 23, 24e10 33874 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x
( ph  ->  ps )
) ).
26 jao 510 . . . . 5  |-  ( ( -.  ph  ->  A. x
( ph  ->  ps )
)  ->  ( ( ps  ->  A. x ( ph  ->  ps ) )  -> 
( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ) )
2717, 25, 26e11 33868 . . . 4  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ).
28 imor 410 . . . 4  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
29 imbi1 321 . . . . 5  |-  ( ( ( ph  ->  ps ) 
<->  ( -.  ph  \/  ps ) )  ->  (
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
)  <->  ( ( -. 
ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3029biimprcd 225 . . . 4  |-  ( ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
)  ->  ( (
( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )  ->  (
( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3127, 28, 30e10 33874 . . 3  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
323, 31gen11nv 33797 . 2  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
3332in1 33742 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367   A.wal 1396
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-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-vd1 33741  df-vd2 33749
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator