Theorem dfvd1ir 44567

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

Syntax hints:   → wi 4  (   wvd1 44563

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 44564

This theorem is referenced by:  idn1  44568  vd01  44591  in2  44599  int2  44600  gen11nv  44611  gen12  44612  exinst01  44619  exinst11  44620  e1a  44621  el1  44622  e111  44668  e1111  44669  un0.1  44772  un10  44781  un01  44782  sbcoreleleqVD  44852  2uasbanhVD  44904