Theorem syl2an2 687

Description: syl2an 597 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 585	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  3633  reusv2lem3  5342  fvmpt2d  6961  fmptco  7082  fnsnbg  7119  peano5  7844  fczsupp0  8143  suppco  8156  oeworde  8529  xpsnen2g  9008  f1domfi  9115  enfii  9120  dffi3  9344  hartogslem1  9457  ttrcltr  9637  isinffi  9916  fseqdom  9948  indcardi  9963  cfslb  10188  fin23lem31  10265  tsksdom  10679  inaprc  10759  fcdmnn0fsuppg  12497  fznatpl1  13532  fzneuz  13562  fzospliti  13646  modifeq2int  13895  hashimarn  14402  cshwsublen  14758  revco  14796  rtrclreclem3  15022  summolem2a  15677  fsum  15682  prodmolem2a  15899  fprod  15906  fzocongeq  16293  odd2np1lem  16309  divalgmod  16375  gcdcllem1  16468  eucalginv  16553  lcmfunsnlem2  16609  lcmflefac  16617  cncongr2  16637  gsumwspan  18814  orbsta  19288  efgredeu  19727  frlmbasfsupp  21738  frlmbasmap  21739  psdmul  22132  mamufacex  22361  matinvgcell  22400  2basgen  22955  ppttop  22972  ordtbaslem  23153  2ndc1stc  23416  xkopt  23620  cnflf2  23968  ngptgp  24601  xmetdcn2  24803  cncfcdm  24865  minveclem3b  25395  mbfeqalem1  25608  limcmpt  25850  ply1divex  26102  elplyd  26167  taylfval  26324  cxpeq  26721  rlimcnp  26929  muval1  27096  lgsval2lem  27270  dchrisum0flblem2  27472  dchrisum0  27483  cutlt  27924  axlowdimlem16  29026  usgr1v  29325  cplgr2vpr  29502  vtxdg0e  29543  wlknewwlksn  29955  wwlksnextwrd  29965  wwlksnwwlksnon  29983  clwlkclwwlklem2a4  30067  numclwwlk8  30462  imadifxp  32671  esum2dlem  34236  fv1stcnv  35959  bj-restsnss  37395  bj-restsnss2  37396  irrdiff  37640  domalom  37720  poimirlem16  37957  poimirlem17  37958  ftc1cnnc  38013  f1o2d2  42674  readvrec2  42793  omcl2  43761  k0004lem3  44576  fvmpt2df  45701  xlimpnfxnegmnf  46242  funressnbrafv2  47692  fpprmod  48203  isubgriedg  48339  isubgrvtx  48343  isubgr3stgrlem2  48443  gpgusgralem  48532