Theorem e12 44715

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

Syntax hints:   → wi 4  (   wvd1 44561  (   wvd2 44569

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 207  df-an 396  df-vd1 44562  df-vd2 44570

This theorem is referenced by:  e12an  44716  trsspwALT  44809  sspwtr  44812  pwtrVD  44815  snssiALTVD  44818  elex2VD  44829  elex22VD  44830  eqsbc2VD  44831  en3lplem1VD  44834  3ornot23VD  44838  orbi1rVD  44839  19.21a3con13vVD  44843  exbirVD  44844  tratrbVD  44852  ssralv2VD  44857  sbcim2gVD  44866  sbcbiVD  44867  relopabVD  44892  19.41rgVD  44893  ax6e2eqVD  44898  ax6e2ndeqVD  44900  vk15.4jVD  44905  con3ALTVD  44907