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

Theorem hbimpgVD 37341
Description: Virtual deduction proof of hbimpg 36965. 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 36965 is hbimpgVD 37341 without virtual deductions and was automatically derived from hbimpgVD 37341. (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 1989 . . . 4  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (
ph  ->  A. x ph )
)
2 hba1 1989 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x ( ps  ->  A. x ps ) )
31, 2hban 2025 . . 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 37035 . . . . . . . 8  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  -.  ph ).
5 idn1 36987 . . . . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ph  ->  A. x ph ) )
75, 6e1a 37049 . . . . . . . . . 10  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
8 hbntal 36964 . . . . . . . . . 10  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x ( -.  ph  ->  A. x  -.  ph ) )
97, 8e1a 37049 . . . . . . . . 9  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x  -.  ph ) ).
10 sp 1948 . . . . . . . . 9  |-  ( A. x ( -.  ph  ->  A. x  -.  ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
119, 10e1a 37049 . . . . . . . 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 37157 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x  -.  ph ).
14 pm2.21 112 . . . . . . . 8  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
1514alimi 1695 . . . . . . 7  |-  ( A. x  -.  ph  ->  A. x
( ph  ->  ps )
)
1613, 15e2 37053 . . . . . 6  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,.  -.  ph  ->.  A. x
( ph  ->  ps ) ).
1716in2 37027 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x
( ph  ->  ps )
) ).
18 simpr 467 . . . . . . . 8  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
->  A. x ps )
)  ->  A. x
( ps  ->  A. x ps ) )
195, 18e1a 37049 . . . . . . 7  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
20 sp 1948 . . . . . . 7  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ps  ->  A. x ps ) )
2119, 20e1a 37049 . . . . . 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 1695 . . . . . 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 37116 . . . . 5  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x
( ph  ->  ps )
) ).
26 jao 519 . . . . 5  |-  ( ( -.  ph  ->  A. x
( ph  ->  ps )
)  ->  ( ( ps  ->  A. x ( ph  ->  ps ) )  -> 
( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ) )
2717, 25, 26e11 37110 . . . 4  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
) ).
28 imor 418 . . . 4  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
29 imbi1 329 . . . . 5  |-  ( ( ( ph  ->  ps ) 
<->  ( -.  ph  \/  ps ) )  ->  (
( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
)  <->  ( ( -. 
ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3029biimprcd 233 . . . 4  |-  ( ( ( -.  ph  \/  ps )  ->  A. x
( ph  ->  ps )
)  ->  ( (
( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )  ->  (
( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ) )
3127, 28, 30e10 37116 . . 3  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
323, 31gen11nv 37039 . 2  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x
( ph  ->  ps )
) ).
3332in1 36984 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 189    \/ wo 374    /\ wa 375   A.wal 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-vd1 36983  df-vd2 36991
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator