Theorem e12 43974

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

Syntax hints:   → wi 4  (   wvd1 43819  (   wvd2 43827

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 396  df-vd1 43820  df-vd2 43828

This theorem is referenced by:  e12an  43975  trsspwALT  44068  sspwtr  44071  pwtrVD  44074  snssiALTVD  44077  elex2VD  44088  elex22VD  44089  eqsbc2VD  44090  en3lplem1VD  44093  3ornot23VD  44097  orbi1rVD  44098  19.21a3con13vVD  44102  exbirVD  44103  tratrbVD  44111  ssralv2VD  44116  sbcim2gVD  44125  sbcbiVD  44126  relopabVD  44151  19.41rgVD  44152  ax6e2eqVD  44157  ax6e2ndeqVD  44159  vk15.4jVD  44164  con3ALTVD  44166