Theorem dfvd1ir 44598

Description: Inference form of df-vd1 44595 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 44595	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbir 231	1 ⊢ (   𝜑   ▶   𝜓   )

Syntax hints:   → wi 4  (   wvd1 44594

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 44595

This theorem is referenced by:  idn1  44599  vd01  44622  in2  44630  int2  44631  gen11nv  44642  gen12  44643  exinst01  44650  exinst11  44651  e1a  44652  el1  44653  e111  44699  e1111  44700  un0.1  44803  un10  44812  un01  44813  sbcoreleleqVD  44883  2uasbanhVD  44935