Theorem e2 45076

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

Syntax hints:   → wi 4  (   wvd2 45022

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 207  df-an 396  df-vd2 45023

This theorem is referenced by:  e2bi  45077  e2bir  45078  sspwtr  45265  pwtrVD  45268  pwtrrVD  45269  suctrALT2VD  45280  tpid3gVD  45286  en3lplem1VD  45287  3ornot23VD  45291  orbi1rVD  45292  19.21a3con13vVD  45296  tratrbVD  45305  syl5impVD  45307  ssralv2VD  45310  truniALTVD  45322  trintALTVD  45324  onfrALTlem3VD  45331  onfrALTlem2VD  45333  onfrALTlem1VD  45334  relopabVD  45345  19.41rgVD  45346  hbimpgVD  45348  ax6e2eqVD  45351  ax6e2ndeqVD  45353  sb5ALTVD  45357  vk15.4jVD  45358  con3ALTVD  45360