Theorem e12 44762

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

Syntax hints:   → wi 4  (   wvd1 44608  (   wvd2 44616

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 44609  df-vd2 44617

This theorem is referenced by:  e12an  44763  trsspwALT  44856  sspwtr  44859  pwtrVD  44862  snssiALTVD  44865  elex2VD  44876  elex22VD  44877  eqsbc2VD  44878  en3lplem1VD  44881  3ornot23VD  44885  orbi1rVD  44886  19.21a3con13vVD  44890  exbirVD  44891  tratrbVD  44899  ssralv2VD  44904  sbcim2gVD  44913  sbcbiVD  44914  relopabVD  44939  19.41rgVD  44940  ax6e2eqVD  44945  ax6e2ndeqVD  44947  vk15.4jVD  44952  con3ALTVD  44954