Theorem e12 44713

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

Syntax hints:   → wi 4  (   wvd1 44559  (   wvd2 44567

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 44560  df-vd2 44568

This theorem is referenced by:  e12an  44714  trsspwALT  44807  sspwtr  44810  pwtrVD  44813  snssiALTVD  44816  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  en3lplem1VD  44832  3ornot23VD  44836  orbi1rVD  44837  19.21a3con13vVD  44841  exbirVD  44842  tratrbVD  44850  ssralv2VD  44855  sbcim2gVD  44864  sbcbiVD  44865  relopabVD  44890  19.41rgVD  44891  ax6e2eqVD  44896  ax6e2ndeqVD  44898  vk15.4jVD  44903  con3ALTVD  44905