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  3658  reusv2lem3  5355  fvmpt2d  6981  fmptco  7101  fnsnbg  7138  peano5  7869  fczsupp0  8172  suppco  8185  oeworde  8557  xpsnen2g  9034  f1domfi  9145  enfii  9150  dffi3  9382  hartogslem1  9495  ttrcltr  9669  isinffi  9945  fseqdom  9979  indcardi  9994  cfslb  10219  fin23lem31  10296  tsksdom  10709  inaprc  10789  fcdmnn0fsuppg  12502  fznatpl1  13539  fzneuz  13569  fzospliti  13652  modifeq2int  13898  hashimarn  14405  cshwsublen  14761  revco  14800  rtrclreclem3  15026  summolem2a  15681  fsum  15686  prodmolem2a  15900  fprod  15907  fzocongeq  16294  odd2np1lem  16310  divalgmod  16376  gcdcllem1  16469  eucalginv  16554  lcmfunsnlem2  16610  lcmflefac  16618  cncongr2  16638  gsumwspan  18773  orbsta  19245  efgredeu  19682  frlmbasfsupp  21667  frlmbasmap  21668  psdmul  22053  mamufacex  22283  matinvgcell  22322  2basgen  22877  ppttop  22894  ordtbaslem  23075  2ndc1stc  23338  xkopt  23542  cnflf2  23890  ngptgp  24524  xmetdcn2  24726  cncfcdm  24791  minveclem3b  25328  mbfeqalem1  25542  limcmpt  25784  ply1divex  26042  elplyd  26107  taylfval  26266  cxpeq  26667  rlimcnp  26875  muval1  27043  lgsval2lem  27218  dchrisum0flblem2  27420  dchrisum0  27431  cutlt  27840  axlowdimlem16  28884  usgr1v  29183  cplgr2vpr  29360  vtxdg0e  29402  wlknewwlksn  29817  wwlksnextwrd  29827  wwlksnwwlksnon  29845  clwlkclwwlklem2a4  29926  numclwwlk8  30321  imadifxp  32530  esum2dlem  34082  fv1stcnv  35764  bj-restsnss  37071  bj-restsnss2  37072  irrdiff  37314  domalom  37392  poimirlem16  37630  poimirlem17  37631  ftc1cnnc  37686  f1o2d2  42221  readvrec2  42349  omcl2  43322  k0004lem3  44138  fvmpt2df  45266  xlimpnfxnegmnf  45812  funressnbrafv2  47245  fpprmod  47728  isubgriedg  47863  isubgrvtx  47867  isubgr3stgrlem2  47966  gpgusgralem  48047