Theorem e2 45373

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

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

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 45320

This theorem is used by:  e2bi  45374  e2bir  45375  sspwtr  45562  pwtrVD  45565  pwtrrVD  45566  suctrALT2VD  45577  tpid3gVD  45583  en3lplem1VD  45584  3ornot23VD  45588  orbi1rVD  45589  19.21a3con13vVD  45593  tratrbVD  45602  syl5impVD  45604  ssralv2VD  45607  truniALTVD  45619  trintALTVD  45621  onfrALTlem3VD  45628  onfrALTlem2VD  45630  onfrALTlem1VD  45631  relopabVD  45642  19.41rgVD  45643  hbimpgVD  45645  ax6e2eqVD  45648  ax6e2ndeqVD  45650  sb5ALTVD  45654  vk15.4jVD  45655  con3ALTVD  45657