Theorem e2 44872

Description: A virtual deduction elimination rule. syl6 35 is e2 44872 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 44826	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		e2.2	. . 3 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	4	dfvd2ir 44827	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd2 44818

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 207  df-an 396  df-vd2 44819

This theorem is referenced by:  e2bi  44873  e2bir  44874  sspwtr  45061  pwtrVD  45064  pwtrrVD  45065  suctrALT2VD  45076  tpid3gVD  45082  en3lplem1VD  45083  3ornot23VD  45087  orbi1rVD  45088  19.21a3con13vVD  45092  tratrbVD  45101  syl5impVD  45103  ssralv2VD  45106  truniALTVD  45118  trintALTVD  45120  onfrALTlem3VD  45127  onfrALTlem2VD  45129  onfrALTlem1VD  45130  relopabVD  45141  19.41rgVD  45142  hbimpgVD  45144  ax6e2eqVD  45147  ax6e2ndeqVD  45149  sb5ALTVD  45153  vk15.4jVD  45154  con3ALTVD  45156