Theorem e2 45690

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

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

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 45637

This theorem is used by:  e2bi  45691  e2bir  45692  sspwtr  45879  pwtrVD  45882  pwtrrVD  45883  suctrALT2VD  45894  tpid3gVD  45900  en3lplem1VD  45901  3ornot23VD  45905  orbi1rVD  45906  19.21a3con13vVD  45910  tratrbVD  45919  syl5impVD  45921  ssralv2VD  45924  truniALTVD  45936  trintALTVD  45938  onfrALTlem3VD  45945  onfrALTlem2VD  45947  onfrALTlem1VD  45948  relopabVD  45959  19.41rgVD  45960  hbimpgVD  45962  ax6e2eqVD  45965  ax6e2ndeqVD  45967  sb5ALTVD  45971  vk15.4jVD  45972  con3ALTVD  45974