Theorem e12 39422

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

Syntax hints:   → wi 4  (   wvd1 39256  (   wvd2 39264

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 197  df-an 385  df-vd1 39257  df-vd2 39265

This theorem is referenced by:  e12an  39423  trsspwALT  39516  sspwtr  39519  pwtrVD  39527  snssiALTVD  39530  elex2VD  39541  elex22VD  39542  eqsbc3rVD  39543  en3lplem1VD  39546  3ornot23VD  39550  orbi1rVD  39551  19.21a3con13vVD  39555  exbirVD  39556  tratrbVD  39565  ssralv2VD  39570  sbcim2gVD  39579  sbcbiVD  39580  relopabVD  39605  19.41rgVD  39606  ax6e2eqVD  39611  ax6e2ndeqVD  39613  vk15.4jVD  39618  con3ALTVD  39620