Theorem e2 44602

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

Syntax hints:   → wi 4  (   wvd2 44548

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 44549

This theorem is referenced by:  e2bi  44603  e2bir  44604  sspwtr  44792  pwtrVD  44795  pwtrrVD  44796  suctrALT2VD  44807  tpid3gVD  44813  en3lplem1VD  44814  3ornot23VD  44818  orbi1rVD  44819  19.21a3con13vVD  44823  tratrbVD  44832  syl5impVD  44834  ssralv2VD  44837  truniALTVD  44849  trintALTVD  44851  onfrALTlem3VD  44858  onfrALTlem2VD  44860  onfrALTlem1VD  44861  relopabVD  44872  19.41rgVD  44873  hbimpgVD  44875  ax6e2eqVD  44878  ax6e2ndeqVD  44880  sb5ALTVD  44884  vk15.4jVD  44885  con3ALTVD  44887