Theorem syl2an2 685

Description: syl2an 598 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 587	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 210  df-an 400

This theorem is referenced by:  elrab3t  3603  reusv2lem3  5272  fvmpt2d  6776  fmptco  6887  peano5  7609  fczsupp0  7872  suppco  7885  oeworde  8234  xpsnen2g  8636  dffi3  8933  hartogslem1  9044  isinffi  9459  fseqdom  9491  indcardi  9506  cfslb  9731  fin23lem31  9808  tsksdom  10221  inaprc  10301  frnnn0fsuppg  11998  fznatpl1  13015  fzneuz  13042  fzospliti  13123  modifeq2int  13355  hashimarn  13856  cshwsublen  14210  revco  14248  rtrclreclem3  14472  summolem2a  15125  fsum  15130  prodmolem2a  15341  fprod  15348  fzocongeq  15730  odd2np1lem  15746  divalgmod  15812  gcdcllem1  15903  eucalginv  15985  lcmfunsnlem2  16041  lcmflefac  16049  cncongr2  16069  gsumwspan  18082  orbsta  18515  efgredeu  18950  frlmbasfsupp  20528  frlmbasmap  20529  mamufacex  21096  matinvgcell  21140  2basgen  21695  ppttop  21712  ordtbaslem  21893  2ndc1stc  22156  xkopt  22360  cnflf2  22708  ngptgp  23343  xmetdcn2  23543  cncffvrn  23604  minveclem3b  24133  mbfeqalem1  24346  limcmpt  24587  ply1divex  24841  elplyd  24903  taylfval  25058  cxpeq  25450  rlimcnp  25655  muval1  25822  lgsval2lem  25995  dchrisum0flblem2  26197  dchrisum0  26208  axlowdimlem16  26855  usgr1v  27150  cplgr2vpr  27327  vtxdg0e  27368  wlknewwlksn  27777  wwlksnextwrd  27787  wwlksnwwlksnon  27805  clwlkclwwlklem2a4  27886  numclwwlk8  28281  imadifxp  30467  esum2dlem  31583  fv1stcnv  33271  bj-restsnss  34804  bj-restsnss2  34805  irrdiff  35046  domalom  35127  poimirlem16  35379  poimirlem17  35380  ftc1cnnc  35435  fnsnbt  39743  k0004lem3  41253  xlimpnfxnegmnf  42850  funressnbrafv2  44196  fpprmod  44640