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

Theorem dfvd1ir 33083
Description: Inference form of df-vd1 33080 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 33080 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbir 209 1  |-  (. ph  ->.  ps
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33079
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 185  df-vd1 33080
This theorem is referenced by:  idn1  33084  vd01  33116  in2  33124  int2  33125  gen11nv  33136  gen12  33137  exinst01  33144  exinst11  33145  e1a  33146  el1  33147  e111  33193  e1111  33194  un0.1  33309  un10  33318  un01  33319  2uasbanhVD  33444
  Copyright terms: Public domain W3C validator