Theorem syl2an2 696

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  elrab3t  3649  reusv2lem3  5356  fvmpt2d  6985  fmptco  7107  fnsnbg  7144  peano5  7870  mpof1o2d  8100  fczsupp0  8168  suppco  8181  oeworde  8558  xpsnen2g  9038  f1domfi  9145  enfii  9150  dffi3  9374  hartogslem1  9487  ttrcltr  9668  isinffi  9947  fseqdom  9979  indcardi  9994  cfslb  10220  fin23lem31  10297  tsksdom  10711  inaprc  10791  fcdmnn0fsuppg  12538  fznatpl1  13580  fzneuz  13610  fzospliti  13694  modifeq2int  13943  hashimarn  14450  cshwsublen  14806  revco  14844  rtrclreclem3  15070  summolem2a  15725  fsum  15730  prodmolem2a  15947  fprod  15954  fzocongeq  16341  odd2np1lem  16357  divalgmod  16423  gcdcllem1  16516  eucalginv  16601  lcmfunsnlem2  16657  lcmflefac  16665  cncongr2  16685  gsumwspan  18863  orbsta  19336  efgredeu  19775  frlmbasfsupp  21790  frlmbasmap  21791  psdmul  22211  mamufacex  22436  matinvgcell  22475  2basgen  23030  ppttop  23047  ordtbaslem  23228  2ndc1stc  23491  xkopt  23695  cnflf2  24043  ngptgp  24676  xmetdcn2  24878  cncfcdm  24940  minveclem3b  25470  mbfeqalem1  25683  limcmpt  25925  ply1divex  26177  elplyd  26242  taylfval  26399  cxpeq  26799  rlimcnp  27007  muval1  27174  lgsval2lem  27348  dchrisum0flblem2  27550  dchrisum0  27561  cutlt  28002  axlowdimlem16  29104  usgr1v  29403  cplgr2vpr  29580  vtxdg0e  29621  wlknewwlksn  30033  wwlksnextwrd  30043  wwlksnwwlksnon  30061  clwlkclwwlklem2a4  30145  numclwwlk8  30540  imadifxp  32750  esum2dlem  34350  fv1stcnv  36091  bj-restsnss  37537  bj-restsnss2  37538  irrdiff  37782  domalom  37862  poimirlem16  38099  poimirlem17  38100  ftc1cnnc  38155  readvrec2  42934  omcl2  43874  k0004lem3  44689  fvmpt2df  45811  xlimpnfxnegmnf  46352  funressnbrafv2  47802  fpprmod  48313  isubgriedg  48449  isubgrvtx  48453  isubgr3stgrlem2  48553  gpgusgralem  48642