Theorem dfvd1ir 42193

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

Syntax hints:   → wi 4  (   wvd1 42189

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 42190

This theorem is referenced by:  idn1  42194  vd01  42217  in2  42225  int2  42226  gen11nv  42237  gen12  42238  exinst01  42245  exinst11  42246  e1a  42247  el1  42248  e111  42294  e1111  42295  un0.1  42399  un10  42408  un01  42409  sbcoreleleqVD  42479  2uasbanhVD  42531