Theorem e12 42233

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

Syntax hints:   → wi 4  (   wvd1 42078  (   wvd2 42086

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 42079  df-vd2 42087

This theorem is referenced by:  e12an  42234  trsspwALT  42327  sspwtr  42330  pwtrVD  42333  snssiALTVD  42336  elex2VD  42347  elex22VD  42348  eqsbc2VD  42349  en3lplem1VD  42352  3ornot23VD  42356  orbi1rVD  42357  19.21a3con13vVD  42361  exbirVD  42362  tratrbVD  42370  ssralv2VD  42375  sbcim2gVD  42384  sbcbiVD  42385  relopabVD  42410  19.41rgVD  42411  ax6e2eqVD  42416  ax6e2ndeqVD  42418  vk15.4jVD  42423  con3ALTVD  42425