Theorem e2 40985

Description: A virtual deduction elimination rule. syl6 35 is e2 40985 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e2.1	⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
e2.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
e2	⊢ (   𝜑   ,   𝜓   ▶   𝜃   )

Proof of Theorem e2

Step	Hyp	Ref	Expression
1		e2.1	. . . 4 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
2	1	dfvd2i 40939	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		e2.2	. . 3 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	4	dfvd2ir 40940	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd2 40931

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 209  df-an 399  df-vd2 40932

This theorem is referenced by:  e2bi  40986  e2bir  40987  sspwtr  41175  pwtrVD  41178  pwtrrVD  41179  suctrALT2VD  41190  tpid3gVD  41196  en3lplem1VD  41197  3ornot23VD  41201  orbi1rVD  41202  19.21a3con13vVD  41206  tratrbVD  41215  syl5impVD  41217  ssralv2VD  41220  truniALTVD  41232  trintALTVD  41234  onfrALTlem3VD  41241  onfrALTlem2VD  41243  onfrALTlem1VD  41244  relopabVD  41255  19.41rgVD  41256  hbimpgVD  41258  ax6e2eqVD  41261  ax6e2ndeqVD  41263  sb5ALTVD  41267  vk15.4jVD  41268  con3ALTVD  41270