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

Theorem hbalgVD 29017
Description: Virtual deduction proof of hbalg 28642. 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 28642 is hbalgVD 29017 without virtual deductions and was automatically derived from hbalgVD 29017. (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 1804 . . 3  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (
ph  ->  A. x ph )
)
2 idn1 28665 . . . . 5  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( ph  ->  A. x ph ) ).
3 ax-5 1566 . . . . 5  |-  ( A. y ( ph  ->  A. x ph )  -> 
( A. y ph  ->  A. y A. x ph ) )
42, 3e1_ 28728 . . . 4  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
5 ax-7 1749 . . . 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 28795 . . 3  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
81, 7gen11nv 28718 . 2  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y
( A. y ph  ->  A. x A. y ph ) ).
98in1 28662 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 1549
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-vd1 28661
  Copyright terms: Public domain W3C validator