Theorem e12 37972

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

Syntax hints:   → wi 4  (   wvd1 37806  (   wvd2 37814

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 196  df-an 385  df-vd1 37807  df-vd2 37815

This theorem is referenced by:  e12an  37973  trsspwALT  38067  sspwtr  38070  pwtrVD  38081  snssiALTVD  38084  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  en3lplem1VD  38100  3ornot23VD  38104  orbi1rVD  38105  19.21a3con13vVD  38109  exbirVD  38110  tratrbVD  38119  ssralv2VD  38124  sbcim2gVD  38133  sbcbiVD  38134  relopabVD  38159  19.41rgVD  38160  ax6e2eqVD  38165  ax6e2ndeqVD  38167  vk15.4jVD  38172  con3ALTVD  38174