Theorem dfvd1ir 42146

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

Syntax hints:   → wi 4  (   wvd1 42142

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 42143

This theorem is referenced by:  idn1  42147  vd01  42170  in2  42178  int2  42179  gen11nv  42190  gen12  42191  exinst01  42198  exinst11  42199  e1a  42200  el1  42201  e111  42247  e1111  42248  un0.1  42352  un10  42361  un01  42362  sbcoreleleqVD  42432  2uasbanhVD  42484