Theorem dfvd1ir 42082

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

Syntax hints:   → wi 4  (   wvd1 42078

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 42079

This theorem is referenced by:  idn1  42083  vd01  42106  in2  42114  int2  42115  gen11nv  42126  gen12  42127  exinst01  42134  exinst11  42135  e1a  42136  el1  42137  e111  42183  e1111  42184  un0.1  42288  un10  42297  un01  42298  sbcoreleleqVD  42368  2uasbanhVD  42420