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 44593
Description: Inference form of df-vd1 44590 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 44590 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbir 231 1 (   𝜑   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44589
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 207  df-vd1 44590
This theorem is referenced by:  idn1  44594  vd01  44617  in2  44625  int2  44626  gen11nv  44637  gen12  44638  exinst01  44645  exinst11  44646  e1a  44647  el1  44648  e111  44694  e1111  44695  un0.1  44799  un10  44808  un01  44809  sbcoreleleqVD  44879  2uasbanhVD  44931
  Copyright terms: Public domain W3C validator