Theorem e12 42344

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

Syntax hints:   → wi 4  (   wvd1 42189  (   wvd2 42197

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 206  df-an 397  df-vd1 42190  df-vd2 42198

This theorem is referenced by:  e12an  42345  trsspwALT  42438  sspwtr  42441  pwtrVD  42444  snssiALTVD  42447  elex2VD  42458  elex22VD  42459  eqsbc2VD  42460  en3lplem1VD  42463  3ornot23VD  42467  orbi1rVD  42468  19.21a3con13vVD  42472  exbirVD  42473  tratrbVD  42481  ssralv2VD  42486  sbcim2gVD  42495  sbcbiVD  42496  relopabVD  42521  19.41rgVD  42522  ax6e2eqVD  42527  ax6e2ndeqVD  42529  vk15.4jVD  42534  con3ALTVD  42536