Theorem e2 44621

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

Syntax hints:   → wi 4  (   wvd2 44567

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 44568

This theorem is referenced by:  e2bi  44622  e2bir  44623  sspwtr  44810  pwtrVD  44813  pwtrrVD  44814  suctrALT2VD  44825  tpid3gVD  44831  en3lplem1VD  44832  3ornot23VD  44836  orbi1rVD  44837  19.21a3con13vVD  44841  tratrbVD  44850  syl5impVD  44852  ssralv2VD  44855  truniALTVD  44867  trintALTVD  44869  onfrALTlem3VD  44876  onfrALTlem2VD  44878  onfrALTlem1VD  44879  relopabVD  44890  19.41rgVD  44891  hbimpgVD  44893  ax6e2eqVD  44896  ax6e2ndeqVD  44898  sb5ALTVD  44902  vk15.4jVD  44903  con3ALTVD  44905