Theorem dfvd1ir 44570

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

Syntax hints:   → wi 4  (   wvd1 44566

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 44567

This theorem is referenced by:  idn1  44571  vd01  44594  in2  44602  int2  44603  gen11nv  44614  gen12  44615  exinst01  44622  exinst11  44623  e1a  44624  el1  44625  e111  44671  e1111  44672  un0.1  44775  un10  44784  un01  44785  sbcoreleleqVD  44855  2uasbanhVD  44907