Theorem e2 45058

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

Syntax hints:   → wi 4  (   wvd2 45004

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 45005

This theorem is referenced by:  e2bi  45059  e2bir  45060  sspwtr  45247  pwtrVD  45250  pwtrrVD  45251  suctrALT2VD  45262  tpid3gVD  45268  en3lplem1VD  45269  3ornot23VD  45273  orbi1rVD  45274  19.21a3con13vVD  45278  tratrbVD  45287  syl5impVD  45289  ssralv2VD  45292  truniALTVD  45304  trintALTVD  45306  onfrALTlem3VD  45313  onfrALTlem2VD  45315  onfrALTlem1VD  45316  relopabVD  45327  19.41rgVD  45328  hbimpgVD  45330  ax6e2eqVD  45333  ax6e2ndeqVD  45335  sb5ALTVD  45339  vk15.4jVD  45340  con3ALTVD  45342