Theorem dfvd1ir 44988

Description: Inference form of df-vd1 44985 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

Step	Hyp	Ref	Expression
1		dfvd1ir.1	. 2 ⊢ (𝜑 → 𝜓)
2		df-vd1 44985	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbir 231	1 ⊢ (   𝜑   ▶   𝜓   )

Syntax hints:   → wi 4  (   wvd1 44984

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 44985

This theorem is referenced by:  idn1  44989  vd01  45012  in2  45020  int2  45021  gen11nv  45032  gen12  45033  exinst01  45040  exinst11  45041  e1a  45042  el1  45043  e111  45089  e1111  45090  un0.1  45193  un10  45202  un01  45203  sbcoreleleqVD  45273  2uasbanhVD  45325