Theorem e2 45708

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

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

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 45655

This theorem is used by:  e2bi  45709  e2bir  45710  sspwtr  45897  pwtrVD  45900  pwtrrVD  45901  suctrALT2VD  45912  tpid3gVD  45918  en3lplem1VD  45919  3ornot23VD  45923  orbi1rVD  45924  19.21a3con13vVD  45928  tratrbVD  45937  syl5impVD  45939  ssralv2VD  45942  truniALTVD  45954  trintALTVD  45956  onfrALTlem3VD  45963  onfrALTlem2VD  45965  onfrALTlem1VD  45966  relopabVD  45977  19.41rgVD  45978  hbimpgVD  45980  ax6e2eqVD  45983  ax6e2ndeqVD  45985  sb5ALTVD  45989  vk15.4jVD  45990  con3ALTVD  45992