Theorem e12 45473

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45319  (   wvd2 45327

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 45320  df-vd2 45328

This theorem is used by:  e12an  45474  trsspwALT  45567  sspwtr  45570  pwtrVD  45573  snssiALTVD  45576  elex2VD  45587  elex22VD  45588  eqsbc2VD  45589  en3lplem1VD  45592  3ornot23VD  45596  orbi1rVD  45597  19.21a3con13vVD  45601  exbirVD  45602  tratrbVD  45610  ssralv2VD  45615  sbcim2gVD  45624  sbcbiVD  45625  relopabVD  45650  19.41rgVD  45651  ax6e2eqVD  45656  ax6e2ndeqVD  45658  vk15.4jVD  45663  con3ALTVD  45665