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 40784
Description: Inference form of df-vd1 40781 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 40781 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbir 232 1 (   𝜑   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 40780
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 208  df-vd1 40781
This theorem is referenced by:  idn1  40785  vd01  40808  in2  40816  int2  40817  gen11nv  40828  gen12  40829  exinst01  40836  exinst11  40837  e1a  40838  el1  40839  e111  40885  e1111  40886  un0.1  40990  un10  40999  un01  41000  sbcoreleleqVD  41070  2uasbanhVD  41122
  Copyright terms: Public domain W3C validator