Theorem e2 42251

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

Syntax hints:   → wi 4  (   wvd2 42197

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 206  df-an 397  df-vd2 42198

This theorem is referenced by:  e2bi  42252  e2bir  42253  sspwtr  42441  pwtrVD  42444  pwtrrVD  42445  suctrALT2VD  42456  tpid3gVD  42462  en3lplem1VD  42463  3ornot23VD  42467  orbi1rVD  42468  19.21a3con13vVD  42472  tratrbVD  42481  syl5impVD  42483  ssralv2VD  42486  truniALTVD  42498  trintALTVD  42500  onfrALTlem3VD  42507  onfrALTlem2VD  42509  onfrALTlem1VD  42510  relopabVD  42521  19.41rgVD  42522  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndeqVD  42529  sb5ALTVD  42533  vk15.4jVD  42534  con3ALTVD  42536