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  3645  reusv2lem3  5345  fvmpt2d  6954  fmptco  7074  fnsnbg  7110  peano5  7835  fczsupp0  8135  suppco  8148  oeworde  8521  xpsnen2g  8998  f1domfi  9105  enfii  9110  dffi3  9334  hartogslem1  9447  ttrcltr  9625  isinffi  9904  fseqdom  9936  indcardi  9951  cfslb  10176  fin23lem31  10253  tsksdom  10667  inaprc  10747  fcdmnn0fsuppg  12461  fznatpl1  13494  fzneuz  13524  fzospliti  13607  modifeq2int  13856  hashimarn  14363  cshwsublen  14719  revco  14757  rtrclreclem3  14983  summolem2a  15638  fsum  15643  prodmolem2a  15857  fprod  15864  fzocongeq  16251  odd2np1lem  16267  divalgmod  16333  gcdcllem1  16426  eucalginv  16511  lcmfunsnlem2  16567  lcmflefac  16575  cncongr2  16595  gsumwspan  18771  orbsta  19242  efgredeu  19681  frlmbasfsupp  21713  frlmbasmap  21714  psdmul  22109  mamufacex  22340  matinvgcell  22379  2basgen  22934  ppttop  22951  ordtbaslem  23132  2ndc1stc  23395  xkopt  23599  cnflf2  23947  ngptgp  24580  xmetdcn2  24782  cncfcdm  24847  minveclem3b  25384  mbfeqalem1  25598  limcmpt  25840  ply1divex  26098  elplyd  26163  taylfval  26322  cxpeq  26723  rlimcnp  26931  muval1  27099  lgsval2lem  27274  dchrisum0flblem2  27476  dchrisum0  27487  cutlt  27928  axlowdimlem16  29030  usgr1v  29329  cplgr2vpr  29506  vtxdg0e  29548  wlknewwlksn  29960  wwlksnextwrd  29970  wwlksnwwlksnon  29988  clwlkclwwlklem2a4  30072  numclwwlk8  30467  imadifxp  32676  esum2dlem  34249  fv1stcnv  35971  bj-restsnss  37284  bj-restsnss2  37285  irrdiff  37527  domalom  37605  poimirlem16  37833  poimirlem17  37834  ftc1cnnc  37889  f1o2d2  42485  readvrec2  42612  omcl2  43571  k0004lem3  44386  fvmpt2df  45512  xlimpnfxnegmnf  46054  funressnbrafv2  47486  fpprmod  47969  isubgriedg  48105  isubgrvtx  48109  isubgr3stgrlem2  48209  gpgusgralem  48298