Theorem e2 41789

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

Syntax hints:   → wi 4  (   wvd2 41735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-vd2 41736

This theorem is referenced by:  e2bi  41790  e2bir  41791  sspwtr  41979  pwtrVD  41982  pwtrrVD  41983  suctrALT2VD  41994  tpid3gVD  42000  en3lplem1VD  42001  3ornot23VD  42005  orbi1rVD  42006  19.21a3con13vVD  42010  tratrbVD  42019  syl5impVD  42021  ssralv2VD  42024  truniALTVD  42036  trintALTVD  42038  onfrALTlem3VD  42045  onfrALTlem2VD  42047  onfrALTlem1VD  42048  relopabVD  42059  19.41rgVD  42060  hbimpgVD  42062  ax6e2eqVD  42065  ax6e2ndeqVD  42067  sb5ALTVD  42071  vk15.4jVD  42072  con3ALTVD  42074