Theorem e2 42140

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

Syntax hints:   → wi 4  (   wvd2 42086

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 206  df-an 396  df-vd2 42087

This theorem is referenced by:  e2bi  42141  e2bir  42142  sspwtr  42330  pwtrVD  42333  pwtrrVD  42334  suctrALT2VD  42345  tpid3gVD  42351  en3lplem1VD  42352  3ornot23VD  42356  orbi1rVD  42357  19.21a3con13vVD  42361  tratrbVD  42370  syl5impVD  42372  ssralv2VD  42375  truniALTVD  42387  trintALTVD  42389  onfrALTlem3VD  42396  onfrALTlem2VD  42398  onfrALTlem1VD  42399  relopabVD  42410  19.41rgVD  42411  hbimpgVD  42413  ax6e2eqVD  42416  ax6e2ndeqVD  42418  sb5ALTVD  42422  vk15.4jVD  42423  con3ALTVD  42425