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

Theorem hbalgVD 28681
Description: Virtual deduction proof of hbalg 28321. 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. hbalg 28321 is hbalgVD 28681 without virtual deductions and was automatically derived from hbalgVD 28681. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y ( ph  ->  A. x ph ) ).
2:1:  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
3::  |-  ( A. y A. x ph  ->  A. x A. y ph )
4:2,3:  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
5::  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (  ph  ->  A. x ph ) )
6:5,4:  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y ( A.  y ph  ->  A. x A. y ph ) ).
qed:6:  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y ( A. y  ph  ->  A. x A. y ph ) )
Assertion
Ref Expression
hbalgVD  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y ( A. y ph  ->  A. x A. y ph ) )

Proof of Theorem hbalgVD
StepHypRef Expression
1 hba1 1719 . . 3  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (
ph  ->  A. x ph )
)
2 idn1 28342 . . . . 5  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( ph  ->  A. x ph ) ).
3 ax-5 1544 . . . . 5  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. y A. x ph ) )
42, 3e1_ 28399 . . . 4  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
5 ax-7 1708 . . . 4  |-  ( A. y A. x ph  ->  A. x A. y ph )
6 imim1 70 . . . 4  |-  ( ( A. y ph  ->  A. y A. x ph )  ->  ( ( A. y A. x ph  ->  A. x A. y ph )  ->  ( A. y ph  ->  A. x A. y ph ) ) )
74, 5, 6e10 28467 . . 3  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
81, 7gen11nv 28389 . 2  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( A. y ph  ->  A. x A. y ph ) ).
98in1 28339 1  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y ( A. y ph  ->  A. x A. y ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   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-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-vd1 28338
  Copyright terms: Public domain W3C validator