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

Theorem hbimpgVD 36941
Description: Virtual deduction proof of hbimpg 36558. 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 36558 is hbimpgVD 36941 without virtual deductions and was automatically derived from hbimpgVD 36941. (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 1953 . . . 4  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (
ph  ->  A. x ph )
)
2 hba1 1953 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x ( ps  ->  A. x ps ) )
31, 2hban 1989 . . 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 36630 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  -.  ph ).
5 idn1 36582 . . . . . . . . . . 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 458 . . . . . . . . . . 11  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ph  ->  A. x ph ) )
75, 6e1a 36644 . . . . . . . . . 10  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
8 hbntal 36557 . . . . . . . . . 10  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
97, 8e1a 36644 . . . . . . . . 9  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
10 sp 1912 . . . . . . . . 9  |-  ( A. x ( -.  ph  ->  A. x  -.  ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
119, 10e1a 36644 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x  -.  ph ) ).
12 pm2.27 40 . . . . . . . 8  |-  ( -. 
ph  ->  ( ( -. 
ph  ->  A. x  -.  ph )  ->  A. x  -.  ph ) )
134, 11, 12e21 36757 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x  -.  ph ).
14 pm2.21 111 . . . . . . . 8  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
1514alimi 1680 . . . . . . 7  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  ps )
)
1613, 15e2 36648 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x
( ph  ->  ps ) ).
1716in2 36622 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x
( ph  ->  ps )
) ).
18 simpr 462 . . . . . . . 8  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ps  ->  A. x ps ) )
195, 18e1a 36644 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
20 sp 1912 . . . . . . 7  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
2119, 20e1a 36644 . . . . . 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 1680 . . . . . 6  |-  ( A. x ps  ->  A. x
( ph  ->  ps )
)
24 imim1 79 . . . . . 6  |-  ( ( ps  ->  A. x ps )  ->  ( ( A. x ps  ->  A. x ( ph  ->  ps ) )  ->  ( ps  ->  A. x ( ph  ->  ps ) ) ) )
2521, 23, 24e10 36711 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x
( ph  ->  ps )
) ).
26 jao 514 . . . . 5  |-  ( ( -.  ph  ->  A. x
( ph  ->  ps )
)  ->  ( ( ps  ->  A. x ( ph  ->  ps ) )  -> 
( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ) )
2717, 25, 26e11 36705 . . . 4  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ).
28 imor 413 . . . 4  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
29 imbi1 324 . . . . 5  |-  ( ( ( ph  ->  ps ) 
<->  ( -.  ph  \/  ps ) )  ->  (
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
)  <->  ( ( -. 
ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3029biimprcd 228 . . . 4  |-  ( ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
)  ->  ( (
( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )  ->  (
( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3127, 28, 30e10 36711 . . 3  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
323, 31gen11nv 36634 . 2  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
3332in1 36579 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 187    \/ wo 369    /\ wa 370   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-vd1 36578  df-vd2 36586
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator