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

Theorem hbalgVD 28726
Description: Virtual deduction proof of hbalg 28353. 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 28353 is hbalgVD 28726 without virtual deductions and was automatically derived from hbalgVD 28726. (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 1800 . . 3  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (
ph  ->  A. x ph )
)
2 idn1 28374 . . . . 5  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( ph  ->  A. x ph ) ).
3 ax-5 1563 . . . . 5  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. y A. x ph ) )
42, 3e1_ 28437 . . . 4  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
5 ax-7 1745 . . . 4  |-  ( A. y A. x ph  ->  A. x A. y ph )
6 imim1 72 . . . 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 28504 . . 3  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
81, 7gen11nv 28427 . 2  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( A. y ph  ->  A. x A. y ph ) ).
98in1 28371 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 1546
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-vd1 28370
  Copyright terms: Public domain W3C validator