Theorem e2 45168

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

Syntax hints:   → wi 4  (   wvd2 45114

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 400  df-vd2 45115

This theorem is referenced by:  e2bi  45169  e2bir  45170  sspwtr  45357  pwtrVD  45360  pwtrrVD  45361  suctrALT2VD  45372  tpid3gVD  45378  en3lplem1VD  45379  3ornot23VD  45383  orbi1rVD  45384  19.21a3con13vVD  45388  tratrbVD  45397  syl5impVD  45399  ssralv2VD  45402  truniALTVD  45414  trintALTVD  45416  onfrALTlem3VD  45423  onfrALTlem2VD  45425  onfrALTlem1VD  45426  relopabVD  45437  19.41rgVD  45438  hbimpgVD  45440  ax6e2eqVD  45443  ax6e2ndeqVD  45445  sb5ALTVD  45449  vk15.4jVD  45450  con3ALTVD  45452