Theorem e12 42717

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

Syntax hints:   → wi 4  (   wvd1 42562  (   wvd2 42570

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-an 397  df-vd1 42563  df-vd2 42571

This theorem is referenced by:  e12an  42718  trsspwALT  42811  sspwtr  42814  pwtrVD  42817  snssiALTVD  42820  elex2VD  42831  elex22VD  42832  eqsbc2VD  42833  en3lplem1VD  42836  3ornot23VD  42840  orbi1rVD  42841  19.21a3con13vVD  42845  exbirVD  42846  tratrbVD  42854  ssralv2VD  42859  sbcim2gVD  42868  sbcbiVD  42869  relopabVD  42894  19.41rgVD  42895  ax6e2eqVD  42900  ax6e2ndeqVD  42902  vk15.4jVD  42907  con3ALTVD  42909