Theorem e12 45705

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45551  (   wvd2 45559

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 45552  df-vd2 45560

This theorem is used by:  e12an  45706  trsspwALT  45799  sspwtr  45802  pwtrVD  45805  snssiALTVD  45808  elex2VD  45819  elex22VD  45820  eqsbc2VD  45821  en3lplem1VD  45824  3ornot23VD  45828  orbi1rVD  45829  19.21a3con13vVD  45833  exbirVD  45834  tratrbVD  45842  ssralv2VD  45847  sbcim2gVD  45856  sbcbiVD  45857  relopabVD  45882  19.41rgVD  45883  ax6e2eqVD  45888  ax6e2ndeqVD  45890  vk15.4jVD  45895  con3ALTVD  45897