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 42947
Description: Inference form of df-vd1 42944 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 42944 . 2 ((   𝜑   ▶   𝜓   ) ↔ (𝜑𝜓))
31, 2mpbir 230 1 (   𝜑   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 42943
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 206  df-vd1 42944
This theorem is referenced by:  idn1  42948  vd01  42971  in2  42979  int2  42980  gen11nv  42991  gen12  42992  exinst01  42999  exinst11  43000  e1a  43001  el1  43002  e111  43048  e1111  43049  un0.1  43153  un10  43162  un01  43163  sbcoreleleqVD  43233  2uasbanhVD  43285
  Copyright terms: Public domain W3C validator