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

Theorem dfvd1ir 36585
Description: Inference form of df-vd1 36582 with the virtual deduction as the assertion. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
dfvd1ir.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
dfvd1ir  |-  (. ph  ->.  ps
).

Proof of Theorem dfvd1ir
StepHypRef Expression
1 dfvd1ir.1 . 2  |-  ( ph  ->  ps )
2 df-vd1 36582 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbir 212 1  |-  (. ph  ->.  ps
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-vd1 36582
This theorem is referenced by:  idn1  36586  vd01  36618  in2  36626  int2  36627  gen11nv  36638  gen12  36639  exinst01  36646  exinst11  36647  e1a  36648  el1  36649  e111  36695  e1111  36696  un0.1  36810  un10  36819  un01  36820  2uasbanhVD  36952
  Copyright terms: Public domain W3C validator