Theorem e12 44700

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

Syntax hints:   → wi 4  (   wvd1 44546  (   wvd2 44554

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 44547  df-vd2 44555

This theorem is referenced by:  e12an  44701  trsspwALT  44794  sspwtr  44797  pwtrVD  44800  snssiALTVD  44803  elex2VD  44814  elex22VD  44815  eqsbc2VD  44816  en3lplem1VD  44819  3ornot23VD  44823  orbi1rVD  44824  19.21a3con13vVD  44828  exbirVD  44829  tratrbVD  44837  ssralv2VD  44842  sbcim2gVD  44851  sbcbiVD  44852  relopabVD  44877  19.41rgVD  44878  ax6e2eqVD  44883  ax6e2ndeqVD  44885  vk15.4jVD  44890  con3ALTVD  44892