Theorem e2 45454

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

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

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 45401

This theorem is used by:  e2bi  45455  e2bir  45456  sspwtr  45643  pwtrVD  45646  pwtrrVD  45647  suctrALT2VD  45658  tpid3gVD  45664  en3lplem1VD  45665  3ornot23VD  45669  orbi1rVD  45670  19.21a3con13vVD  45674  tratrbVD  45683  syl5impVD  45685  ssralv2VD  45688  truniALTVD  45700  trintALTVD  45702  onfrALTlem3VD  45709  onfrALTlem2VD  45711  onfrALTlem1VD  45712  relopabVD  45723  19.41rgVD  45724  hbimpgVD  45726  ax6e2eqVD  45729  ax6e2ndeqVD  45731  sb5ALTVD  45735  vk15.4jVD  45736  con3ALTVD  45738