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

Theorem dfvd1ir 33744
Description: Inference form of df-vd1 33741 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 33741 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbir 209 1  |-  (. ph  ->.  ps
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33740
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 33741
This theorem is referenced by:  idn1  33745  vd01  33777  in2  33785  int2  33786  gen11nv  33797  gen12  33798  exinst01  33805  exinst11  33806  e1a  33807  el1  33808  e111  33854  e1111  33855  un0.1  33970  un10  33979  un01  33980  2uasbanhVD  34112
  Copyright terms: Public domain W3C validator