Theorem e2 41337

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

Syntax hints:   → wi 4  (   wvd2 41283

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 210  df-an 400  df-vd2 41284

This theorem is referenced by:  e2bi  41338  e2bir  41339  sspwtr  41527  pwtrVD  41530  pwtrrVD  41531  suctrALT2VD  41542  tpid3gVD  41548  en3lplem1VD  41549  3ornot23VD  41553  orbi1rVD  41554  19.21a3con13vVD  41558  tratrbVD  41567  syl5impVD  41569  ssralv2VD  41572  truniALTVD  41584  trintALTVD  41586  onfrALTlem3VD  41593  onfrALTlem2VD  41595  onfrALTlem1VD  41596  relopabVD  41607  19.41rgVD  41608  hbimpgVD  41610  ax6e2eqVD  41613  ax6e2ndeqVD  41615  sb5ALTVD  41619  vk15.4jVD  41620  con3ALTVD  41622