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

Theorem dfvd1ir 37604
Description: Inference form of df-vd1 37601 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 (𝜑𝜓)
Assertion
Ref Expression
dfvd1ir (   𝜑   ▶   𝜓   )

Proof of Theorem dfvd1ir
StepHypRef Expression
1 dfvd1ir.1 . 2 (𝜑𝜓)
2 df-vd1 37601 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbir 220 1 (   𝜑   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 37600
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 196  df-vd1 37601
This theorem is referenced by:  idn1  37605  vd01  37637  in2  37645  int2  37646  gen11nv  37657  gen12  37658  exinst01  37665  exinst11  37666  e1a  37667  el1  37668  e111  37714  e1111  37715  un0.1  37821  un10  37830  un01  37831  2uasbanhVD  37963
  Copyright terms: Public domain W3C validator