MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2an2 Structured version   Visualization version   GIF version

Theorem syl2an2 910
Description: syl2an 495 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2.1 (𝜑𝜓)
syl2an2.2 ((𝜒𝜑) → 𝜃)
syl2an2.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2 ((𝜒𝜑) → 𝜏)

Proof of Theorem syl2an2
StepHypRef Expression
1 syl2an2.1 . . 3 (𝜑𝜓)
2 syl2an2.2 . . 3 ((𝜒𝜑) → 𝜃)
3 syl2an2.3 . . 3 ((𝜓𝜃) → 𝜏)
41, 2, 3syl2an 495 . 2 ((𝜑 ∧ (𝜒𝜑)) → 𝜏)
54anabss7 897 1 ((𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  elrab3t  3504  reusv2lem3  5021  fvmpt2d  6457  fmptco  6561  fseqdom  9060  hashimarn  13440  divalgmod  15352  lcmfunsnlem2  15576  lcmflefac  15584  cncongr2  15605  usgr1v  26369  cplgr2vpr  26561  vtxdg0e  26602  wlknewwlksn  27018  wwlksnextwrd  27037  wwlksnwwlksnon  27055  wwlksnwwlksnonOLD  27057  clwlkclwwlklem2a4  27142  numclwwlk8  27582  esum2dlem  30485  fv1stcnv  32007  bj-restsnss  33361  bj-restsnss2  33362  k0004lem3  38968
  Copyright terms: Public domain W3C validator