Theorem e12 41958

Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e12.1	⊢ (   𝜑   ▶   𝜓   )
e12.2	⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
e12.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
e12	⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Proof of Theorem e12

Step	Hyp	Ref	Expression
1		e12.1	. . 3 ⊢ (   𝜑   ▶   𝜓   )
2	1	vd12 41834	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 41905	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd1 41803  (   wvd2 41811

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 210  df-an 400  df-vd1 41804  df-vd2 41812

This theorem is referenced by:  e12an  41959  trsspwALT  42052  sspwtr  42055  pwtrVD  42058  snssiALTVD  42061  elex2VD  42072  elex22VD  42073  eqsbc3rVD  42074  en3lplem1VD  42077  3ornot23VD  42081  orbi1rVD  42082  19.21a3con13vVD  42086  exbirVD  42087  tratrbVD  42095  ssralv2VD  42100  sbcim2gVD  42109  sbcbiVD  42110  relopabVD  42135  19.41rgVD  42136  ax6e2eqVD  42141  ax6e2ndeqVD  42143  vk15.4jVD  42148  con3ALTVD  42150