Theorem dfvd1ir 44544

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

Syntax hints:   → wi 4  (   wvd1 44540

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 44541

This theorem is referenced by:  idn1  44545  vd01  44568  in2  44576  int2  44577  gen11nv  44588  gen12  44589  exinst01  44596  exinst11  44597  e1a  44598  el1  44599  e111  44645  e1111  44646  un0.1  44750  un10  44759  un01  44760  sbcoreleleqVD  44830  2uasbanhVD  44882