Theorem e2 44984

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

Syntax hints:   → wi 4  (   wvd2 44930

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 44931

This theorem is referenced by:  e2bi  44985  e2bir  44986  sspwtr  45173  pwtrVD  45176  pwtrrVD  45177  suctrALT2VD  45188  tpid3gVD  45194  en3lplem1VD  45195  3ornot23VD  45199  orbi1rVD  45200  19.21a3con13vVD  45204  tratrbVD  45213  syl5impVD  45215  ssralv2VD  45218  truniALTVD  45230  trintALTVD  45232  onfrALTlem3VD  45239  onfrALTlem2VD  45241  onfrALTlem1VD  45242  relopabVD  45253  19.41rgVD  45254  hbimpgVD  45256  ax6e2eqVD  45259  ax6e2ndeqVD  45261  sb5ALTVD  45265  vk15.4jVD  45266  con3ALTVD  45268