Theorem syl2an2 699

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elrab3t  3647  reusv2lem3  5369  fvmpt2d  7004  fmptco  7127  fnsnbg  7166  peano5  7894  mpof1o2d  8127  fczsupp0  8195  suppco  8208  oeworde  8585  xpsnen2g  9072  f1domfi  9179  enfii  9184  dffi3  9405  hartogslem1  9518  ttrcltr  9699  isinffi  10001  fseqdom  10033  indcardi  10048  cfslb  10272  fin23lem31  10349  tsksdom  10769  inaprc  10849  fcdmnn0fsuppg  12592  fznatpl1  13637  fzneuz  13667  fzospliti  13751  modifeq2int  14001  hashimarn  14509  cshwsublen  14871  revco  14909  rtrclreclem3  15137  summolem2a  15805  fsum  15810  prodmolem2a  16027  fprod  16034  fzocongeq  16420  odd2np1lem  16436  divalgmod  16502  gcdcllem1  16595  eucalginv  16680  lcmfunsnlem2  16736  lcmflefac  16744  cncongr2  16764  gsumwspan  18961  orbsta  19446  efgredeu  19885  frlmbasfsupp  21977  frlmbasmap  21978  psdmul  22400  mamufacex  22624  matinvgcell  22663  2basgen  23221  ppttop  23238  ordtbaslem  23419  2ndc1stc  23682  xkopt  23887  cnflf2  24235  ngptgp  24868  xmetdcn2  25070  cncfcdm  25132  minveclem3b  25662  mbfeqalem1  25875  limcmpt  26117  ply1divex  26369  elplyd  26434  taylfval  26602  cxpeq  27002  rlimcnp  27210  muval1  27377  lgsval2lem  27551  dchrisum0flblem2  27753  dchrisum0  27764  cutlt  28205  axlowdimlem16  29422  usgr1v  29724  cplgr2vpr  29901  vtxdg0e  29942  wlknewwlksn  30363  wwlksnextwrd  30373  wwlksnwwlksnon  30391  clwlkclwwlklem2a4  30475  numclwwlk8  30880  imadifxp  33082  esum2dlem  34610  fv1stcnv  36364  bj-restsnss  37841  bj-restsnss2  37842  irrdiff  38086  domalom  38166  poimirlem16  38393  poimirlem17  38394  ftc1cnnc  38449  readvrec2  43244  omcl2  44182  k0004lem3  44997  fvmpt2df  46109  xlimpnfxnegmnf  46650  funressnbrafv2  48140  fpprmod  48651  isubgriedg  48787  isubgrvtx  48791  isubgr3stgrlem2  48891  gpgusgralem  48980