Theorem e2 44664

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

Syntax hints:   → wi 4  (   wvd2 44610

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 44611

This theorem is referenced by:  e2bi  44665  e2bir  44666  sspwtr  44853  pwtrVD  44856  pwtrrVD  44857  suctrALT2VD  44868  tpid3gVD  44874  en3lplem1VD  44875  3ornot23VD  44879  orbi1rVD  44880  19.21a3con13vVD  44884  tratrbVD  44893  syl5impVD  44895  ssralv2VD  44898  truniALTVD  44910  trintALTVD  44912  onfrALTlem3VD  44919  onfrALTlem2VD  44921  onfrALTlem1VD  44922  relopabVD  44933  19.41rgVD  44934  hbimpgVD  44936  ax6e2eqVD  44939  ax6e2ndeqVD  44941  sb5ALTVD  44945  vk15.4jVD  44946  con3ALTVD  44948