Theorem syl2an2 692

Description: syl2an 602 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 590	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  3635  reusv2lem3  5336  fvmpt2d  6956  fmptco  7078  fnsnbg  7115  peano5  7840  mpof1o2d  8072  fczsupp0  8140  suppco  8153  oeworde  8526  xpsnen2g  9005  f1domfi  9112  enfii  9117  dffi3  9341  hartogslem1  9454  ttrcltr  9635  isinffi  9914  fseqdom  9946  indcardi  9961  cfslb  10186  fin23lem31  10263  tsksdom  10677  inaprc  10757  fcdmnn0fsuppg  12495  fznatpl1  13530  fzneuz  13560  fzospliti  13644  modifeq2int  13893  hashimarn  14400  cshwsublen  14756  revco  14794  rtrclreclem3  15020  summolem2a  15675  fsum  15680  prodmolem2a  15897  fprod  15904  fzocongeq  16291  odd2np1lem  16307  divalgmod  16373  gcdcllem1  16466  eucalginv  16551  lcmfunsnlem2  16607  lcmflefac  16615  cncongr2  16635  gsumwspan  18812  orbsta  19286  efgredeu  19725  frlmbasfsupp  21740  frlmbasmap  21741  psdmul  22161  mamufacex  22386  matinvgcell  22425  2basgen  22980  ppttop  22997  ordtbaslem  23178  2ndc1stc  23441  xkopt  23645  cnflf2  23993  ngptgp  24626  xmetdcn2  24828  cncfcdm  24890  minveclem3b  25420  mbfeqalem1  25633  limcmpt  25875  ply1divex  26127  elplyd  26192  taylfval  26349  cxpeq  26746  rlimcnp  26954  muval1  27121  lgsval2lem  27295  dchrisum0flblem2  27497  dchrisum0  27508  cutlt  27949  axlowdimlem16  29051  usgr1v  29350  cplgr2vpr  29527  vtxdg0e  29568  wlknewwlksn  29980  wwlksnextwrd  29990  wwlksnwwlksnon  30008  clwlkclwwlklem2a4  30092  numclwwlk8  30487  imadifxp  32697  esum2dlem  34283  fv1stcnv  36012  bj-restsnss  37448  bj-restsnss2  37449  irrdiff  37693  domalom  37773  poimirlem16  38010  poimirlem17  38011  ftc1cnnc  38066  readvrec2  42845  omcl2  43785  k0004lem3  44600  fvmpt2df  45723  xlimpnfxnegmnf  46264  funressnbrafv2  47714  fpprmod  48225  isubgriedg  48361  isubgrvtx  48365  isubgr3stgrlem2  48465  gpgusgralem  48554