Theorem e2 40972

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

Syntax hints:   → wi 4  (   wvd2 40918

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 209  df-an 399  df-vd2 40919

This theorem is referenced by:  e2bi  40973  e2bir  40974  sspwtr  41162  pwtrVD  41165  pwtrrVD  41166  suctrALT2VD  41177  tpid3gVD  41183  en3lplem1VD  41184  3ornot23VD  41188  orbi1rVD  41189  19.21a3con13vVD  41193  tratrbVD  41202  syl5impVD  41204  ssralv2VD  41207  truniALTVD  41219  trintALTVD  41221  onfrALTlem3VD  41228  onfrALTlem2VD  41230  onfrALTlem1VD  41231  relopabVD  41242  19.41rgVD  41243  hbimpgVD  41245  ax6e2eqVD  41248  ax6e2ndeqVD  41250  sb5ALTVD  41254  vk15.4jVD  41255  con3ALTVD  41257