Theorem syl2an2 682

Description: syl2an 595 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

Step	Hyp	Ref	Expression
1		syl2an2.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 482	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 584	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  elrab3t  3617  reusv2lem3  5192  fvmpt2d  6647  fmptco  6754  peano5  7461  fczsupp0  7710  suppco  7721  oeworde  8069  xpsnen2g  8457  dffi3  8741  hartogslem1  8852  isinffi  9267  fseqdom  9298  indcardi  9313  cfslb  9534  fin23lem31  9611  tsksdom  10024  inaprc  10104  fznatpl1  12811  fzneuz  12838  fzospliti  12919  modifeq2int  13151  hashimarn  13649  swrdccatin2  13927  cshwsublen  13994  revco  14032  rtrclreclem3  14253  summolem2a  14905  fsum  14910  prodmolem2a  15121  fprod  15128  fzocongeq  15507  odd2np1lem  15522  divalgmod  15590  gcdcllem1  15681  eucalginv  15757  lcmfunsnlem2  15813  lcmflefac  15821  cncongr2  15841  gsumwspan  17822  orbsta  18184  efgredeu  18605  frlmbasfsupp  20584  frlmbasmap  20585  mamufacex  20682  matinvgcell  20728  2basgen  21282  ppttop  21299  ordtbaslem  21480  2ndc1stc  21743  xkopt  21947  cnflf2  22295  ngptgp  22928  xmetdcn2  23128  cncffvrn  23189  minveclem3b  23714  mbfeqalem1  23925  limcmpt  24164  ply1divex  24413  elplyd  24475  taylfval  24630  cxpeq  25019  rlimcnp  25225  muval1  25392  lgsval2lem  25565  dchrisum0flblem2  25767  dchrisum0  25778  axlowdimlem16  26426  usgr1v  26721  cplgr2vpr  26898  vtxdg0e  26939  wlknewwlksn  27352  wwlksnextwrd  27362  wwlksnwwlksnon  27381  clwlkclwwlklem2a4  27462  numclwwlk8  27863  imadifxp  30041  esum2dlem  30968  fv1stcnv  32629  bj-restsnss  33992  bj-restsnss2  33993  domalom  34235  ftc1cnnc  34516  fnsnbt  38669  k0004lem3  40003  xlimpnfxnegmnf  41656  funressnbrafv2  42979  fpprmod  43394