Theorem e12 45415

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

Syntax hints:   → wi 4  (   wvd1 45261  (   wvd2 45269

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 45262  df-vd2 45270

This theorem is referenced by:  e12an  45416  trsspwALT  45509  sspwtr  45512  pwtrVD  45515  snssiALTVD  45518  elex2VD  45529  elex22VD  45530  eqsbc2VD  45531  en3lplem1VD  45534  3ornot23VD  45538  orbi1rVD  45539  19.21a3con13vVD  45543  exbirVD  45544  tratrbVD  45552  ssralv2VD  45557  sbcim2gVD  45566  sbcbiVD  45567  relopabVD  45592  19.41rgVD  45593  ax6e2eqVD  45598  ax6e2ndeqVD  45600  vk15.4jVD  45605  con3ALTVD  45607