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  3646  reusv2lem3  5338  fvmpt2d  6942  fmptco  7062  fnsnbg  7098  peano5  7823  fczsupp0  8123  suppco  8136  oeworde  8508  xpsnen2g  8983  f1domfi  9090  enfii  9095  dffi3  9315  hartogslem1  9428  ttrcltr  9606  isinffi  9882  fseqdom  9914  indcardi  9929  cfslb  10154  fin23lem31  10231  tsksdom  10644  inaprc  10724  fcdmnn0fsuppg  12438  fznatpl1  13475  fzneuz  13505  fzospliti  13588  modifeq2int  13837  hashimarn  14344  cshwsublen  14700  revco  14738  rtrclreclem3  14964  summolem2a  15619  fsum  15624  prodmolem2a  15838  fprod  15845  fzocongeq  16232  odd2np1lem  16248  divalgmod  16314  gcdcllem1  16407  eucalginv  16492  lcmfunsnlem2  16548  lcmflefac  16556  cncongr2  16576  gsumwspan  18751  orbsta  19223  efgredeu  19662  frlmbasfsupp  21693  frlmbasmap  21694  psdmul  22079  mamufacex  22309  matinvgcell  22348  2basgen  22903  ppttop  22920  ordtbaslem  23101  2ndc1stc  23364  xkopt  23568  cnflf2  23916  ngptgp  24549  xmetdcn2  24751  cncfcdm  24816  minveclem3b  25353  mbfeqalem1  25567  limcmpt  25809  ply1divex  26067  elplyd  26132  taylfval  26291  cxpeq  26692  rlimcnp  26900  muval1  27068  lgsval2lem  27243  dchrisum0flblem2  27445  dchrisum0  27456  cutlt  27874  axlowdimlem16  28933  usgr1v  29232  cplgr2vpr  29409  vtxdg0e  29451  wlknewwlksn  29863  wwlksnextwrd  29873  wwlksnwwlksnon  29891  clwlkclwwlklem2a4  29972  numclwwlk8  30367  imadifxp  32576  esum2dlem  34100  fv1stcnv  35809  bj-restsnss  37116  bj-restsnss2  37117  irrdiff  37359  domalom  37437  poimirlem16  37675  poimirlem17  37676  ftc1cnnc  37731  f1o2d2  42265  readvrec2  42393  omcl2  43365  k0004lem3  44181  fvmpt2df  45308  xlimpnfxnegmnf  45851  funressnbrafv2  47274  fpprmod  47757  isubgriedg  47893  isubgrvtx  47897  isubgr3stgrlem2  47997  gpgusgralem  48086