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

Theorem hbalgVD 28192
Description: Virtual deduction proof of hbalg 27815. 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 27815 is hbalgVD 28192 without virtual deductions and was automatically derived from hbalgVD 28192. (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 1745 . . 3  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (
ph  ->  A. x ph )
)
2 idn1 27836 . . . . 5  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( ph  ->  A. x ph ) ).
3 ax-5 1548 . . . . 5  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. y A. x ph ) )
42, 3e1_ 27899 . . . 4  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
5 ax-7 1725 . . . 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 27967 . . 3  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
81, 7gen11nv 27889 . 2  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( A. y ph  ->  A. x A. y ph ) ).
98in1 27833 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 1531
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-ex 1533  df-vd1 27832
  Copyright terms: Public domain W3C validator