Theorem dfvd1ir 45030

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

Syntax hints:   → wi 4  (   wvd1 45026

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 209  df-vd1 45027

This theorem is referenced by:  idn1  45031  vd01  45054  in2  45062  int2  45063  gen11nv  45074  gen12  45075  exinst01  45082  exinst11  45083  e1a  45084  el1  45085  e111  45131  e1111  45132  un0.1  45235  un10  45244  un01  45245  sbcoreleleqVD  45315  2uasbanhVD  45367