Theorem dfvd1ir 44851

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

Syntax hints:   → wi 4  (   wvd1 44847

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 44848

This theorem is referenced by:  idn1  44852  vd01  44875  in2  44883  int2  44884  gen11nv  44895  gen12  44896  exinst01  44903  exinst11  44904  e1a  44905  el1  44906  e111  44952  e1111  44953  un0.1  45056  un10  45065  un01  45066  sbcoreleleqVD  45136  2uasbanhVD  45188