Theorem e2 44594

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

Syntax hints:   → wi 4  (   wvd2 44540

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 44541

This theorem is referenced by:  e2bi  44595  e2bir  44596  sspwtr  44783  pwtrVD  44786  pwtrrVD  44787  suctrALT2VD  44798  tpid3gVD  44804  en3lplem1VD  44805  3ornot23VD  44809  orbi1rVD  44810  19.21a3con13vVD  44814  tratrbVD  44823  syl5impVD  44825  ssralv2VD  44828  truniALTVD  44840  trintALTVD  44842  onfrALTlem3VD  44849  onfrALTlem2VD  44851  onfrALTlem1VD  44852  relopabVD  44863  19.41rgVD  44864  hbimpgVD  44866  ax6e2eqVD  44869  ax6e2ndeqVD  44871  sb5ALTVD  44875  vk15.4jVD  44876  con3ALTVD  44878