Theorem syl2an2 684

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 484	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 586	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  elrab3t  3679  reusv2lem3  5301  fvmpt2d  6781  fmptco  6891  peano5  7605  fczsupp0  7859  suppco  7870  oeworde  8219  xpsnen2g  8610  dffi3  8895  hartogslem1  9006  isinffi  9421  fseqdom  9452  indcardi  9467  cfslb  9688  fin23lem31  9765  tsksdom  10178  inaprc  10258  fznatpl1  12962  fzneuz  12989  fzospliti  13070  modifeq2int  13302  hashimarn  13802  cshwsublen  14158  revco  14196  rtrclreclem3  14419  summolem2a  15072  fsum  15077  prodmolem2a  15288  fprod  15295  fzocongeq  15674  odd2np1lem  15689  divalgmod  15757  gcdcllem1  15848  eucalginv  15928  lcmfunsnlem2  15984  lcmflefac  15992  cncongr2  16012  gsumwspan  18011  orbsta  18443  efgredeu  18878  frlmbasfsupp  20902  frlmbasmap  20903  mamufacex  21000  matinvgcell  21044  2basgen  21598  ppttop  21615  ordtbaslem  21796  2ndc1stc  22059  xkopt  22263  cnflf2  22611  ngptgp  23245  xmetdcn2  23445  cncffvrn  23506  minveclem3b  24031  mbfeqalem1  24242  limcmpt  24481  ply1divex  24730  elplyd  24792  taylfval  24947  cxpeq  25338  rlimcnp  25543  muval1  25710  lgsval2lem  25883  dchrisum0flblem2  26085  dchrisum0  26096  axlowdimlem16  26743  usgr1v  27038  cplgr2vpr  27215  vtxdg0e  27256  wlknewwlksn  27665  wwlksnextwrd  27675  wwlksnwwlksnon  27694  clwlkclwwlklem2a4  27775  numclwwlk8  28171  imadifxp  30351  esum2dlem  31351  fv1stcnv  33020  bj-restsnss  34377  bj-restsnss2  34378  domalom  34688  ftc1cnnc  34981  fnsnbt  39140  k0004lem3  40519  xlimpnfxnegmnf  42115  funressnbrafv2  43463  fpprmod  43912