Theorem dfvd1ir 44012

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

Syntax hints:   → wi 4  (   wvd1 44008

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 44009

This theorem is referenced by:  idn1  44013  vd01  44036  in2  44044  int2  44045  gen11nv  44056  gen12  44057  exinst01  44064  exinst11  44065  e1a  44066  el1  44067  e111  44113  e1111  44114  un0.1  44218  un10  44227  un01  44228  sbcoreleleqVD  44298  2uasbanhVD  44350