Theorem e12 44964

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

Syntax hints:   → wi 4  (   wvd1 44810  (   wvd2 44818

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 44811  df-vd2 44819

This theorem is referenced by:  e12an  44965  trsspwALT  45058  sspwtr  45061  pwtrVD  45064  snssiALTVD  45067  elex2VD  45078  elex22VD  45079  eqsbc2VD  45080  en3lplem1VD  45083  3ornot23VD  45087  orbi1rVD  45088  19.21a3con13vVD  45092  exbirVD  45093  tratrbVD  45101  ssralv2VD  45106  sbcim2gVD  45115  sbcbiVD  45116  relopabVD  45141  19.41rgVD  45142  ax6e2eqVD  45147  ax6e2ndeqVD  45149  vk15.4jVD  45154  con3ALTVD  45156