Theorem syl2an2 682

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  elrab3t  3616  reusv2lem3  5318  fvmpt2d  6870  fmptco  6983  peano5  7714  peano5OLD  7715  fczsupp0  7980  suppco  7993  oeworde  8386  xpsnen2g  8805  f1domfi  8928  enfii  8932  dffi3  9120  hartogslem1  9231  isinffi  9681  fseqdom  9713  indcardi  9728  cfslb  9953  fin23lem31  10030  tsksdom  10443  inaprc  10523  frnnn0fsuppg  12222  fznatpl1  13239  fzneuz  13266  fzospliti  13347  modifeq2int  13581  hashimarn  14083  cshwsublen  14437  revco  14475  rtrclreclem3  14699  summolem2a  15355  fsum  15360  prodmolem2a  15572  fprod  15579  fzocongeq  15961  odd2np1lem  15977  divalgmod  16043  gcdcllem1  16134  eucalginv  16217  lcmfunsnlem2  16273  lcmflefac  16281  cncongr2  16301  gsumwspan  18400  orbsta  18834  efgredeu  19273  frlmbasfsupp  20875  frlmbasmap  20876  mamufacex  21448  matinvgcell  21492  2basgen  22048  ppttop  22065  ordtbaslem  22247  2ndc1stc  22510  xkopt  22714  cnflf2  23062  ngptgp  23698  xmetdcn2  23906  cncffvrn  23967  minveclem3b  24497  mbfeqalem1  24710  limcmpt  24952  ply1divex  25206  elplyd  25268  taylfval  25423  cxpeq  25815  rlimcnp  26020  muval1  26187  lgsval2lem  26360  dchrisum0flblem2  26562  dchrisum0  26573  axlowdimlem16  27228  usgr1v  27526  cplgr2vpr  27703  vtxdg0e  27744  wlknewwlksn  28153  wwlksnextwrd  28163  wwlksnwwlksnon  28181  clwlkclwwlklem2a4  28262  numclwwlk8  28657  imadifxp  30841  esum2dlem  31960  fv1stcnv  33657  ttrcltr  33702  bj-restsnss  35181  bj-restsnss2  35182  irrdiff  35424  domalom  35502  poimirlem16  35720  poimirlem17  35721  ftc1cnnc  35776  fnsnbt  40134  k0004lem3  41648  xlimpnfxnegmnf  43245  funressnbrafv2  44623  fpprmod  45067