Theorem e12 45291

Description: A virtual deduction elimination rule (see sylsyld 62). (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 45168	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 45239	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd1 45137  (   wvd2 45145

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 401  df-vd1 45138  df-vd2 45146

This theorem is referenced by:  e12an  45292  trsspwALT  45385  sspwtr  45388  pwtrVD  45391  snssiALTVD  45394  elex2VD  45405  elex22VD  45406  eqsbc2VD  45407  en3lplem1VD  45410  3ornot23VD  45414  orbi1rVD  45415  19.21a3con13vVD  45419  exbirVD  45420  tratrbVD  45428  ssralv2VD  45433  sbcim2gVD  45442  sbcbiVD  45443  relopabVD  45468  19.41rgVD  45469  ax6e2eqVD  45474  ax6e2ndeqVD  45476  vk15.4jVD  45481  con3ALTVD  45483