Theorem e2 45874

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

This proof depends on syntax axioms:   → wi 4  (   wvd2 45820

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd2 45821

This theorem is used by:  e2bi  45875  e2bir  45876  sspwtr  46063  pwtrVD  46066  pwtrrVD  46067  suctrALT2VD  46078  tpid3gVD  46084  en3lplem1VD  46085  3ornot23VD  46089  orbi1rVD  46090  19.21a3con13vVD  46094  tratrbVD  46103  syl5impVD  46105  ssralv2VD  46108  truniALTVD  46120  trintALTVD  46122  onfrALTlem3VD  46129  onfrALTlem2VD  46131  onfrALTlem1VD  46132  relopabVD  46143  19.41rgVD  46144  hbimpgVD  46146  ax6e2eqVD  46149  ax6e2ndeqVD  46151  sb5ALTVD  46155  vk15.4jVD  46156  con3ALTVD  46158