Theorem syl2an2 698

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  elrab3t  3650  reusv2lem3  5373  fvmpt2d  7005  fmptco  7127  fnsnbg  7164  peano5  7891  mpof1o2d  8122  fczsupp0  8190  suppco  8203  oeworde  8580  xpsnen2g  9059  f1domfi  9166  enfii  9171  dffi3  9392  hartogslem1  9505  ttrcltr  9686  isinffi  9979  fseqdom  10011  indcardi  10026  cfslb  10251  fin23lem31  10328  tsksdom  10742  inaprc  10822  fcdmnn0fsuppg  12565  fznatpl1  13608  fzneuz  13638  fzospliti  13722  modifeq2int  13971  hashimarn  14479  cshwsublen  14835  revco  14873  rtrclreclem3  15099  summolem2a  15768  fsum  15773  prodmolem2a  15990  fprod  15997  fzocongeq  16383  odd2np1lem  16399  divalgmod  16465  gcdcllem1  16558  eucalginv  16643  lcmfunsnlem2  16699  lcmflefac  16707  cncongr2  16727  gsumwspan  18906  orbsta  19384  efgredeu  19823  frlmbasfsupp  21889  frlmbasmap  21890  psdmul  22310  mamufacex  22534  matinvgcell  22573  2basgen  23128  ppttop  23145  ordtbaslem  23326  2ndc1stc  23589  xkopt  23793  cnflf2  24141  ngptgp  24774  xmetdcn2  24976  cncfcdm  25038  minveclem3b  25568  mbfeqalem1  25781  limcmpt  26023  ply1divex  26275  elplyd  26340  taylfval  26500  cxpeq  26900  rlimcnp  27108  muval1  27275  lgsval2lem  27449  dchrisum0flblem2  27651  dchrisum0  27662  cutlt  28103  axlowdimlem16  29285  usgr1v  29584  cplgr2vpr  29761  vtxdg0e  29802  wlknewwlksn  30214  wwlksnextwrd  30224  wwlksnwwlksnon  30242  clwlkclwwlklem2a4  30326  numclwwlk8  30721  imadifxp  32924  esum2dlem  34460  fv1stcnv  36247  bj-restsnss  37703  bj-restsnss2  37704  irrdiff  37948  domalom  38028  poimirlem16  38265  poimirlem17  38266  ftc1cnnc  38321  readvrec2  43100  omcl2  44040  k0004lem3  44855  fvmpt2df  45967  xlimpnfxnegmnf  46508  funressnbrafv2  47958  fpprmod  48469  isubgriedg  48605  isubgrvtx  48609  isubgr3stgrlem2  48709  gpgusgralem  48798