Theorem e2 45061

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

Syntax hints:   → wi 4  (   wvd2 45007

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 45008

This theorem is referenced by:  e2bi  45062  e2bir  45063  sspwtr  45250  pwtrVD  45253  pwtrrVD  45254  suctrALT2VD  45265  tpid3gVD  45271  en3lplem1VD  45272  3ornot23VD  45276  orbi1rVD  45277  19.21a3con13vVD  45281  tratrbVD  45290  syl5impVD  45292  ssralv2VD  45295  truniALTVD  45307  trintALTVD  45309  onfrALTlem3VD  45316  onfrALTlem2VD  45318  onfrALTlem1VD  45319  relopabVD  45330  19.41rgVD  45331  hbimpgVD  45333  ax6e2eqVD  45336  ax6e2ndeqVD  45338  sb5ALTVD  45342  vk15.4jVD  45343  con3ALTVD  45345