Theorem syl2an2 685

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  elrab3t  3683  reusv2lem3  5399  fvmpt2d  7012  fmptco  7127  peano5  7884  peano5OLD  7885  fczsupp0  8178  suppco  8191  oeworde  8593  xpsnen2g  9065  f1domfi  9184  enfii  9189  dffi3  9426  hartogslem1  9537  ttrcltr  9711  isinffi  9987  fseqdom  10021  indcardi  10036  cfslb  10261  fin23lem31  10338  tsksdom  10751  inaprc  10831  fcdmnn0fsuppg  12531  fznatpl1  13555  fzneuz  13582  fzospliti  13664  modifeq2int  13898  hashimarn  14400  cshwsublen  14746  revco  14785  rtrclreclem3  15007  summolem2a  15661  fsum  15666  prodmolem2a  15878  fprod  15885  fzocongeq  16267  odd2np1lem  16283  divalgmod  16349  gcdcllem1  16440  eucalginv  16521  lcmfunsnlem2  16577  lcmflefac  16585  cncongr2  16605  gsumwspan  18727  orbsta  19177  efgredeu  19620  frlmbasfsupp  21313  frlmbasmap  21314  mamufacex  21891  matinvgcell  21937  2basgen  22493  ppttop  22510  ordtbaslem  22692  2ndc1stc  22955  xkopt  23159  cnflf2  23507  ngptgp  24145  xmetdcn2  24353  cncfcdm  24414  minveclem3b  24945  mbfeqalem1  25158  limcmpt  25400  ply1divex  25654  elplyd  25716  taylfval  25871  cxpeq  26265  rlimcnp  26470  muval1  26637  lgsval2lem  26810  dchrisum0flblem2  27012  dchrisum0  27023  cutlt  27419  axlowdimlem16  28215  usgr1v  28513  cplgr2vpr  28690  vtxdg0e  28731  wlknewwlksn  29141  wwlksnextwrd  29151  wwlksnwwlksnon  29169  clwlkclwwlklem2a4  29250  numclwwlk8  29645  imadifxp  31832  esum2dlem  33090  fv1stcnv  34748  bj-restsnss  35964  bj-restsnss2  35965  irrdiff  36207  domalom  36285  poimirlem16  36504  poimirlem17  36505  ftc1cnnc  36560  fnsnbt  41051  f1o2d2  41055  omcl2  42083  k0004lem3  42900  fvmpt2df  43977  xlimpnfxnegmnf  44530  funressnbrafv2  45952  fpprmod  46395