Theorem e2 45323

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

Syntax hints:   → wi 4  (   wvd2 45269

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 210  df-an 401  df-vd2 45270

This theorem is referenced by:  e2bi  45324  e2bir  45325  sspwtr  45512  pwtrVD  45515  pwtrrVD  45516  suctrALT2VD  45527  tpid3gVD  45533  en3lplem1VD  45534  3ornot23VD  45538  orbi1rVD  45539  19.21a3con13vVD  45543  tratrbVD  45552  syl5impVD  45554  ssralv2VD  45557  truniALTVD  45569  trintALTVD  45571  onfrALTlem3VD  45578  onfrALTlem2VD  45580  onfrALTlem1VD  45581  relopabVD  45592  19.41rgVD  45593  hbimpgVD  45595  ax6e2eqVD  45598  ax6e2ndeqVD  45600  sb5ALTVD  45604  vk15.4jVD  45605  con3ALTVD  45607