Theorem syl2an2 686

Description: syl2an 596 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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 584	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  elrab3t  3691  reusv2lem3  5400  fvmpt2d  7029  fmptco  7149  peano5  7915  fczsupp0  8218  suppco  8231  oeworde  8631  xpsnen2g  9105  f1domfi  9221  enfii  9226  dffi3  9471  hartogslem1  9582  ttrcltr  9756  isinffi  10032  fseqdom  10066  indcardi  10081  cfslb  10306  fin23lem31  10383  tsksdom  10796  inaprc  10876  fcdmnn0fsuppg  12586  fznatpl1  13618  fzneuz  13648  fzospliti  13731  modifeq2int  13974  hashimarn  14479  cshwsublen  14834  revco  14873  rtrclreclem3  15099  summolem2a  15751  fsum  15756  prodmolem2a  15970  fprod  15977  fzocongeq  16361  odd2np1lem  16377  divalgmod  16443  gcdcllem1  16536  eucalginv  16621  lcmfunsnlem2  16677  lcmflefac  16685  cncongr2  16705  gsumwspan  18859  orbsta  19331  efgredeu  19770  frlmbasfsupp  21778  frlmbasmap  21779  psdmul  22170  mamufacex  22400  matinvgcell  22441  2basgen  22997  ppttop  23014  ordtbaslem  23196  2ndc1stc  23459  xkopt  23663  cnflf2  24011  ngptgp  24649  xmetdcn2  24859  cncfcdm  24924  minveclem3b  25462  mbfeqalem1  25676  limcmpt  25918  ply1divex  26176  elplyd  26241  taylfval  26400  cxpeq  26800  rlimcnp  27008  muval1  27176  lgsval2lem  27351  dchrisum0flblem2  27553  dchrisum0  27564  cutlt  27966  axlowdimlem16  28972  usgr1v  29273  cplgr2vpr  29450  vtxdg0e  29492  wlknewwlksn  29907  wwlksnextwrd  29917  wwlksnwwlksnon  29935  clwlkclwwlklem2a4  30016  numclwwlk8  30411  imadifxp  32614  esum2dlem  34093  fv1stcnv  35777  bj-restsnss  37084  bj-restsnss2  37085  irrdiff  37327  domalom  37405  poimirlem16  37643  poimirlem17  37644  ftc1cnnc  37699  fnsnbt  42271  f1o2d2  42274  readvrec2  42391  omcl2  43346  k0004lem3  44162  fvmpt2df  45279  xlimpnfxnegmnf  45829  funressnbrafv2  47256  fpprmod  47714  isubgriedg  47849  isubgrvtx  47853  isubgr3stgrlem2  47934  gpgusgralem  48011