Theorem e12 44749

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

Syntax hints:   → wi 4  (   wvd1 44594  (   wvd2 44602

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 44595  df-vd2 44603

This theorem is referenced by:  e12an  44750  trsspwALT  44843  sspwtr  44846  pwtrVD  44849  snssiALTVD  44852  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  en3lplem1VD  44868  3ornot23VD  44872  orbi1rVD  44873  19.21a3con13vVD  44877  exbirVD  44878  tratrbVD  44886  ssralv2VD  44891  sbcim2gVD  44900  sbcbiVD  44901  relopabVD  44926  19.41rgVD  44927  ax6e2eqVD  44932  ax6e2ndeqVD  44934  vk15.4jVD  44939  con3ALTVD  44941