Theorem e12 45006

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

Syntax hints:   → wi 4  (   wvd1 44852  (   wvd2 44860

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 44853  df-vd2 44861

This theorem is referenced by:  e12an  45007  trsspwALT  45100  sspwtr  45103  pwtrVD  45106  snssiALTVD  45109  elex2VD  45120  elex22VD  45121  eqsbc2VD  45122  en3lplem1VD  45125  3ornot23VD  45129  orbi1rVD  45130  19.21a3con13vVD  45134  exbirVD  45135  tratrbVD  45143  ssralv2VD  45148  sbcim2gVD  45157  sbcbiVD  45158  relopabVD  45183  19.41rgVD  45184  ax6e2eqVD  45189  ax6e2ndeqVD  45191  vk15.4jVD  45196  con3ALTVD  45198