Theorem e2 44623

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

Syntax hints:   → wi 4  (   wvd2 44569

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 44570

This theorem is referenced by:  e2bi  44624  e2bir  44625  sspwtr  44812  pwtrVD  44815  pwtrrVD  44816  suctrALT2VD  44827  tpid3gVD  44833  en3lplem1VD  44834  3ornot23VD  44838  orbi1rVD  44839  19.21a3con13vVD  44843  tratrbVD  44852  syl5impVD  44854  ssralv2VD  44857  truniALTVD  44869  trintALTVD  44871  onfrALTlem3VD  44878  onfrALTlem2VD  44880  onfrALTlem1VD  44881  relopabVD  44892  19.41rgVD  44893  hbimpgVD  44895  ax6e2eqVD  44898  ax6e2ndeqVD  44900  sb5ALTVD  44904  vk15.4jVD  44905  con3ALTVD  44907