Theorem e12 44695

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

Syntax hints:   → wi 4  (   wvd1 44540  (   wvd2 44548

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 44541  df-vd2 44549

This theorem is referenced by:  e12an  44696  trsspwALT  44789  sspwtr  44792  pwtrVD  44795  snssiALTVD  44798  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  en3lplem1VD  44814  3ornot23VD  44818  orbi1rVD  44819  19.21a3con13vVD  44823  exbirVD  44824  tratrbVD  44832  ssralv2VD  44837  sbcim2gVD  44846  sbcbiVD  44847  relopabVD  44872  19.41rgVD  44873  ax6e2eqVD  44878  ax6e2ndeqVD  44880  vk15.4jVD  44885  con3ALTVD  44887