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 39555
Description: Inference form of df-vd1 39552 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 39552 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbir 223 1 (   𝜑   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39551
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 199  df-vd1 39552
This theorem is referenced by:  idn1  39556  vd01  39588  in2  39596  int2  39597  gen11nv  39608  gen12  39609  exinst01  39616  exinst11  39617  e1a  39618  el1  39619  e111  39665  e1111  39666  un0.1  39771  un10  39780  un01  39781  sbcoreleleqVD  39851  2uasbanhVD  39903
  Copyright terms: Public domain W3C validator