Theorem e12 45665

Description: A virtual deduction elimination rule (see sylsyld 62). (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 45542	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 45613	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45511  (   wvd2 45519

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd1 45512  df-vd2 45520

This theorem is used by:  e12an  45666  trsspwALT  45759  sspwtr  45762  pwtrVD  45765  snssiALTVD  45768  elex2VD  45779  elex22VD  45780  eqsbc2VD  45781  en3lplem1VD  45784  3ornot23VD  45788  orbi1rVD  45789  19.21a3con13vVD  45793  exbirVD  45794  tratrbVD  45802  ssralv2VD  45807  sbcim2gVD  45816  sbcbiVD  45817  relopabVD  45842  19.41rgVD  45843  ax6e2eqVD  45848  ax6e2ndeqVD  45850  vk15.4jVD  45855  con3ALTVD  45857