Theorem e2 44788

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

Syntax hints:   → wi 4  (   wvd2 44734

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 44735

This theorem is referenced by:  e2bi  44789  e2bir  44790  sspwtr  44977  pwtrVD  44980  pwtrrVD  44981  suctrALT2VD  44992  tpid3gVD  44998  en3lplem1VD  44999  3ornot23VD  45003  orbi1rVD  45004  19.21a3con13vVD  45008  tratrbVD  45017  syl5impVD  45019  ssralv2VD  45022  truniALTVD  45034  trintALTVD  45036  onfrALTlem3VD  45043  onfrALTlem2VD  45045  onfrALTlem1VD  45046  relopabVD  45057  19.41rgVD  45058  hbimpgVD  45060  ax6e2eqVD  45063  ax6e2ndeqVD  45065  sb5ALTVD  45069  vk15.4jVD  45070  con3ALTVD  45072