Theorem e2 45599

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

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

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 45546

This theorem is used by:  e2bi  45600  e2bir  45601  sspwtr  45788  pwtrVD  45791  pwtrrVD  45792  suctrALT2VD  45803  tpid3gVD  45809  en3lplem1VD  45810  3ornot23VD  45814  orbi1rVD  45815  19.21a3con13vVD  45819  tratrbVD  45828  syl5impVD  45830  ssralv2VD  45833  truniALTVD  45845  trintALTVD  45847  onfrALTlem3VD  45854  onfrALTlem2VD  45856  onfrALTlem1VD  45857  relopabVD  45868  19.41rgVD  45869  hbimpgVD  45871  ax6e2eqVD  45874  ax6e2ndeqVD  45876  sb5ALTVD  45880  vk15.4jVD  45881  con3ALTVD  45883