Theorem e2 45075

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

Syntax hints:   → wi 4  (   wvd2 45021

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 208  df-an 397  df-vd2 45022

This theorem is referenced by:  e2bi  45076  e2bir  45077  sspwtr  45264  pwtrVD  45267  pwtrrVD  45268  suctrALT2VD  45279  tpid3gVD  45285  en3lplem1VD  45286  3ornot23VD  45290  orbi1rVD  45291  19.21a3con13vVD  45295  tratrbVD  45304  syl5impVD  45306  ssralv2VD  45309  truniALTVD  45321  trintALTVD  45323  onfrALTlem3VD  45330  onfrALTlem2VD  45332  onfrALTlem1VD  45333  relopabVD  45344  19.41rgVD  45345  hbimpgVD  45347  ax6e2eqVD  45350  ax6e2ndeqVD  45352  sb5ALTVD  45356  vk15.4jVD  45357  con3ALTVD  45359