Theorem syl2an2 686

Description: syl2an 596 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 584	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 207  df-an 396

This theorem is referenced by:  elrab3t  3649  reusv2lem3  5342  fvmpt2d  6947  fmptco  7067  fnsnbg  7104  peano5  7833  fczsupp0  8133  suppco  8146  oeworde  8518  xpsnen2g  8994  f1domfi  9105  enfii  9110  dffi3  9340  hartogslem1  9453  ttrcltr  9631  isinffi  9907  fseqdom  9939  indcardi  9954  cfslb  10179  fin23lem31  10256  tsksdom  10669  inaprc  10749  fcdmnn0fsuppg  12462  fznatpl1  13499  fzneuz  13529  fzospliti  13612  modifeq2int  13858  hashimarn  14365  cshwsublen  14720  revco  14759  rtrclreclem3  14985  summolem2a  15640  fsum  15645  prodmolem2a  15859  fprod  15866  fzocongeq  16253  odd2np1lem  16269  divalgmod  16335  gcdcllem1  16428  eucalginv  16513  lcmfunsnlem2  16569  lcmflefac  16577  cncongr2  16597  gsumwspan  18738  orbsta  19210  efgredeu  19649  frlmbasfsupp  21683  frlmbasmap  21684  psdmul  22069  mamufacex  22299  matinvgcell  22338  2basgen  22893  ppttop  22910  ordtbaslem  23091  2ndc1stc  23354  xkopt  23558  cnflf2  23906  ngptgp  24540  xmetdcn2  24742  cncfcdm  24807  minveclem3b  25344  mbfeqalem1  25558  limcmpt  25800  ply1divex  26058  elplyd  26123  taylfval  26282  cxpeq  26683  rlimcnp  26891  muval1  27059  lgsval2lem  27234  dchrisum0flblem2  27436  dchrisum0  27447  cutlt  27863  axlowdimlem16  28920  usgr1v  29219  cplgr2vpr  29396  vtxdg0e  29438  wlknewwlksn  29850  wwlksnextwrd  29860  wwlksnwwlksnon  29878  clwlkclwwlklem2a4  29959  numclwwlk8  30354  imadifxp  32563  esum2dlem  34058  fv1stcnv  35749  bj-restsnss  37056  bj-restsnss2  37057  irrdiff  37299  domalom  37377  poimirlem16  37615  poimirlem17  37616  ftc1cnnc  37671  f1o2d2  42206  readvrec2  42334  omcl2  43306  k0004lem3  44122  fvmpt2df  45250  xlimpnfxnegmnf  45796  funressnbrafv2  47229  fpprmod  47712  isubgriedg  47848  isubgrvtx  47852  isubgr3stgrlem2  47952  gpgusgralem  48041