Theorem e12 40515

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 40391	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 40462	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd1 40360  (   wvd2 40368

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 199  df-an 388  df-vd1 40361  df-vd2 40369

This theorem is referenced by:  e12an  40516  trsspwALT  40609  sspwtr  40612  pwtrVD  40615  snssiALTVD  40618  elex2VD  40629  elex22VD  40630  eqsbc3rVD  40631  en3lplem1VD  40634  3ornot23VD  40638  orbi1rVD  40639  19.21a3con13vVD  40643  exbirVD  40644  tratrbVD  40652  ssralv2VD  40657  sbcim2gVD  40666  sbcbiVD  40667  relopabVD  40692  19.41rgVD  40693  ax6e2eqVD  40698  ax6e2ndeqVD  40700  vk15.4jVD  40705  con3ALTVD  40707