Theorem e2 45225

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

Syntax hints:   → wi 4  (   wvd2 45171

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 401  df-vd2 45172

This theorem is referenced by:  e2bi  45226  e2bir  45227  sspwtr  45414  pwtrVD  45417  pwtrrVD  45418  suctrALT2VD  45429  tpid3gVD  45435  en3lplem1VD  45436  3ornot23VD  45440  orbi1rVD  45441  19.21a3con13vVD  45445  tratrbVD  45454  syl5impVD  45456  ssralv2VD  45459  truniALTVD  45471  trintALTVD  45473  onfrALTlem3VD  45480  onfrALTlem2VD  45482  onfrALTlem1VD  45483  relopabVD  45494  19.41rgVD  45495  hbimpgVD  45497  ax6e2eqVD  45500  ax6e2ndeqVD  45502  sb5ALTVD  45506  vk15.4jVD  45507  con3ALTVD  45509