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

Theorem dfvd1ir 36986
Description: Inference form of df-vd1 36983 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 36983 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbir 214 1  |-  (. ph  ->.  ps
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36982
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 190  df-vd1 36983
This theorem is referenced by:  idn1  36987  vd01  37019  in2  37027  int2  37028  gen11nv  37039  gen12  37040  exinst01  37047  exinst11  37048  e1a  37049  el1  37050  e111  37096  e1111  37097  un0.1  37206  un10  37215  un01  37216  2uasbanhVD  37348
  Copyright terms: Public domain W3C validator