Theorem e2 44625

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

Syntax hints:   → wi 4  (   wvd2 44571

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 44572

This theorem is referenced by:  e2bi  44626  e2bir  44627  sspwtr  44814  pwtrVD  44817  pwtrrVD  44818  suctrALT2VD  44829  tpid3gVD  44835  en3lplem1VD  44836  3ornot23VD  44840  orbi1rVD  44841  19.21a3con13vVD  44845  tratrbVD  44854  syl5impVD  44856  ssralv2VD  44859  truniALTVD  44871  trintALTVD  44873  onfrALTlem3VD  44880  onfrALTlem2VD  44882  onfrALTlem1VD  44883  relopabVD  44894  19.41rgVD  44895  hbimpgVD  44897  ax6e2eqVD  44900  ax6e2ndeqVD  44902  sb5ALTVD  44906  vk15.4jVD  44907  con3ALTVD  44909