Theorem syl2an 289

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2an	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 ⊢ (𝜏 → 𝜒)
2		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 283	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 286	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  syl2anr  290  anim12i  338  syl2an2  602  syl2an2r  603  orandc  952  mp3an3an  1384  eqeqan12d  2254  sylan9eq  2291  csbcomg  3170  sylan9ss  3261  ssconb  3362  ineqan12d  3434  dfopg  3902  breqan12d  4146  opexg  4368  copsex2g  4386  ordin  4530  onin  4531  unexg  4589  eusv1  4598  opelvvg  4824  opthprc  4826  opbrop  4854  relop  4930  dmpropg  5260  unixpm  5323  funssres  5420  funinsn  5430  funtp  5434  fnco  5491  resasplitss  5569  fodmrnu  5623  relrnfvex  5713  funopdmsn  5895  fconst2g  5930  oveqan12d  6104  ovi3  6226  ovg  6228  f1opw2  6296  off  6315  offres  6368  suppfnss  6497  iunon  6555  nnsucsssuc  6765  nnaword1  6786  ertr  6822  erex  6831  brecop  6899  ecovdi  6920  ecovidi  6921  mapvalg  6932  pmvalg  6933  pmss12g  6956  mapsn  6972  en2sn  7102  xpf1o  7144  xpen  7145  phplem4  7156  ssfilem  7177  ssfilemd  7179  diffitest  7191  en1eqsn  7265  sbthlem7  7280  fsuppxpfi  7296  ordiso  7376  updjud  7422  fodju0  7487  finnum  7528  pr2nelem  7537  djucomen  7572  exmidontriimlem1  7577  2onetap  7621  ltsopi  7687  pitric  7688  pitri3or  7689  ltdcpi  7690  mulclpi  7695  addcompig  7696  mulcompig  7698  distrpig  7700  ltexpi  7704  ltapig  7705  ltmpig  7706  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enqdc  7728  addcmpblnq  7734  addpipqqslem  7736  mulpipq2  7738  mulpipq  7739  mulpipqqs  7740  addclnq  7742  distrnqg  7754  ltdcnq  7764  ltrnqg  7787  enq0breq  7803  addclnq0  7818  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  distrnq0  7826  mulcomnq0  7827  genipv  7876  genplt2i  7877  genpelvl  7879  genpelvu  7880  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  addnqpr  7928  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  mulnqpr  7944  distrlem4prl  7951  distrlem4pru  7952  ltnqpr  7960  recexprlemloc  7998  archrecnq  8030  mulclsr  8121  1idsr  8135  00sr  8136  prsradd  8153  axmulass  8240  axdistr  8241  axcnre  8248  peano5nnnn  8259  mulrid  8323  axltadd  8395  lenlt  8401  cnegexlem3  8503  cnegex  8504  resubcl  8590  subeqrev  8702  muladd  8711  mulsub  8728  mulsub2  8729  ltaddsub2  8765  leaddsub2  8767  leltadd  8775  ltaddpos2  8781  posdif  8783  addge02  8801  mullt0  8808  recexre  8907  recextlem1  8980  recexap  8982  divmuldivap  9043  conjmulap  9060  div2subap  9168  prodgt02  9184  prodge02  9186  lemul2  9188  lemul2a  9190  ltmulgt12  9196  lemulge12  9198  ltmuldiv2  9206  ltdivmul2  9209  ledivmul2  9211  lemuldiv2  9213  negiso  9286  cju  9292  peano5nni  9308  nnaddcl  9325  nnmulcl  9326  nnsub  9344  addltmul  9544  avgle1  9548  avgle2  9549  nnrecl  9563  nn0nnaddcl  9596  zsubcl  9687  zleloe  9693  znnsub  9698  nzadd  9699  zmulcl  9700  zltp1le  9701  zleltp1  9702  nnleltp1  9706  nnltp1le  9707  nnaddm1cl  9708  nn0ltp1le  9709  nn0leltp1  9710  nn0ltlem1  9711  znn0sub  9712  nn0sub  9713  elz2  9718  zapne  9721  zdcle  9723  zdclt  9724  zltlen  9726  nn0lem1lt  9731  nnlem1lt  9732  nnltlem1  9733  zdiv  9736  zextle  9739  zextlt  9740  btwnnz  9742  prime  9747  nneo  9751  peano2uz2  9755  peano5uzti  9756  uzind  9759  fzind  9763  fnn0ind  9764  uzneg  9943  uz11  9947  eluzp1m1  9948  eluzp1p1  9950  uzin  9957  indstr  9995  uz2mulcl  10010  qre  10027  qaddcl  10037  qsubcl  10040  qltlen  10042  qlttri2  10043  irradd  10048  elpqb  10052  cnref1o  10053  rpaddcl  10080  rpmulcl  10081  rpdivcl  10082  rexadd  10256  rexsub  10257  xaddcom  10265  xnn0xadd0  10271  xnegdi  10272  elicc2  10342  iccshftr  10398  iccshftl  10400  iccdil  10402  icccntr  10404  fzval2  10416  elfz1eq  10441  peano2fzr  10443  fznlem  10447  fzsplit2  10457  fzsplit3  10460  fzaddel  10467  fzsubel  10468  fzrev2  10494  fzrev3  10496  uzsplit  10501  fzrevral  10514  fzrevral3  10516  fzshftral  10517  elfz2nn0  10521  fznn0sub2  10537  fz0fzdiffz0  10539  elfzmlbp  10541  difelfzle  10543  difelfznle  10544  1fv  10548  elfzouz2  10571  fzo0n  10577  fzouzsplit  10590  fzoun  10592  elfzo0le  10599  fzonmapblen  10601  fzofzim  10602  fzoaddel2  10610  eluzgtdifelfzo  10617  elfzodifsumelfzo  10621  ubmelm1fzo  10646  fzofzp1b  10648  fzosplitprm1  10655  fzostep1  10658  subfzo0  10663  zsupcllemstep  10664  qdclt  10682  qbtwnxr  10694  flqbi2  10728  divfl0  10733  flqzadd  10735  flqmulnn0  10736  addmodidr  10812  modfzo0difsn  10834  frec2uzltd  10842  frec2uzrand  10844  frecfzen2  10866  seqshft2g  10921  seq3split  10927  seqsplitg  10928  seq3caopr2  10932  seqcaopr2g  10933  seqf1oglem2  10959  exp3vallem  10979  expcllem  10989  expcl2lemap  10990  1exp  11007  expge1  11015  expadd  11020  expmul  11023  expsubap  11026  leexp1a  11033  lt2sq  11052  le2sq  11053  sumsqeq0  11057  qsqeqor  11089  bernneq  11100  bernneq2  11101  sq11ap  11147  facdiv  11178  faclbnd  11181  faclbnd3  11183  faclbnd6  11184  facavg  11186  bcrpcl  11193  bccmpl  11194  bcm1n  11209  fiubm  11273  seq3coll  11296  eqwrd  11347  ccatcl  11363  ccatclab  11364  ccatlen  11365  ccat0  11366  ccatval1  11367  ccatval2  11368  elfzelfzccat  11370  ccatvalfn  11371  ccatsymb  11372  ccatval21sw  11375  ccatrn  11379  lswccatn0lsw  11381  ccatalpha  11383  ccatrcl1  11384  swrdfv2  11437  swrdsbslen  11440  swrdspsleq  11441  swrdccat2  11445  pfxclz  11453  ccatpfx  11475  pfxccat1  11476  swrdswrdlem  11478  pfxswrd  11480  pfxccatin12lem4  11500  pfxccatin12lem1  11502  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccat3  11508  swrdccat  11509  pfxccatpfx2  11511  pfxccat3a  11512  swrdccat3blem  11513  swrdccat3b  11514  s2dmg  11564  shftfvalg  11585  shftf  11597  crre  11624  crim  11625  mulreap  11631  readd  11636  resub  11637  remul2  11640  imadd  11644  imsub  11645  immul2  11647  ipcnval  11653  cjsub  11659  cjreim  11671  caucvgre  11749  rexanuz  11756  rexuz3  11758  resqrexlemover  11778  resqrexlemcvg  11787  resqrexlemglsq  11790  sqrtle  11804  sqrtlt  11805  sqrt11ap  11806  sqrt11  11807  absreimsq  11835  absreim  11836  absmul  11837  sqabs  11850  absdiflt  11860  absdifle  11861  abssuble0  11871  abs2difabs  11876  fzomaxdif  11881  caubnd2  11885  rpmaxcl  11991  zmaxcl  11992  nn0maxcl  11993  minmax  11998  mincl  11999  min1inf  12000  min2inf  12001  minabs  12004  minclpr  12005  rpmincl  12006  2zinfmin  12011  xrmaxrecl  12023  xrminmax  12033  xrmincl  12034  xrmin1inf  12035  xrmin2inf  12036  xrminrecl  12041  xrminrpcl  12042  iooinsup  12045  climconst2  12059  climuni  12061  2clim  12069  climshft  12072  climshft2  12074  cjcn2  12084  climaddc1  12097  climmulc2  12099  climsubc1  12100  climsubc2  12101  climlec2  12109  summodclem2a  12150  zsumdc  12153  isumclim3  12192  mptfzshft  12211  fsumrev  12212  fisum0diag2  12216  telfsumo2  12236  fsumparts  12239  cvgcmpub  12245  binomlem  12252  binom1p  12254  binom1dif  12256  bcxmas  12258  isumshft  12259  expcnvap0  12271  expcnv  12273  geosergap  12275  geolim  12280  cvgratnnlemrate  12299  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  prodmodc  12347  zproddc  12348  fprodf1o  12357  fprodeq0  12386  efcj  12442  eftlub  12459  effsumlt  12461  efieq  12504  sinsub  12509  cossub  12510  subsin  12512  sinmul  12513  cosmul  12514  addcos  12515  subcos  12516  dvdssub2  12604  dvdsadd  12605  dvdsaddr  12606  dvdssub  12607  dvdssubr  12608  fzocongeq  12627  odd2np1  12642  opoe  12664  omoe  12665  opeo  12666  omeo  12667  divalgb  12694  ndvdsadd  12700  bitsfi  12726  gcdmndc  12734  gcdabs  12767  dvdsgcd  12791  absmulgcd  12796  gcdmultiple  12799  gcdmultiplez  12800  rpmulgcd  12805  sqgcd  12808  dvdssqlem  12809  dvdssq  12810  nninfctlemfo  12819  nn0seqcvgd  12821  ialgrlemconst  12823  algrf  12825  algrp1  12826  algcvg  12828  algcvga  12831  lcmval  12843  lcmabs  12856  lcmgcd  12858  lcmdvds  12859  lcmgcdnn  12862  coprmgcdb  12868  coprmdvds  12872  coprmdvds2  12873  qredeq  12876  isprm3  12898  nprm  12903  divgcdodd  12923  prmdvdsexp  12928  sqrt2irr  12942  zgcdsq  12981  hashdvds  13001  phiprmpw  13002  crth  13004  phimullem  13005  modprm0  13035  coprimeprodsq  13038  coprimeprodsq2  13039  pythagtriplem2  13047  pythagtriplem19  13063  pcdvdsb  13101  pcneg  13106  pc2dvds  13111  pc11  13112  pcmpt  13124  pcfac  13131  infpnlem1  13140  prmunb  13143  1arithlem4  13147  1arith  13148  gzaddcl  13158  gzmulcl  13159  gzreim  13160  gzsubcl  13161  4sqlem1  13169  4sqlem4a  13172  4sqlem4  13173  4sqlem12  13183  ballotfilemfc0  13234  ballotfilemfcc  13235  setsvalg  13384  setsfun0  13390  restval  13601  mndinvmod  13760  resmhm  13796  resmhm2  13797  mhmco  13799  dfgrp3m  13906  mhmmnd  13921  mulgnngzsum  13932  mulgnn0z  13954  mulgnndir  13956  ghmex  14060  0ghm  14063  resghm  14065  resghm2  14066  ghmco  14069  ghmeql  14072  kerf1ghm  14079  ablsubsub23  14131  xpsval  14203  dfrhm2  14463  isrhm  14467  rhmfn  14481  rhmval  14482  rhmco  14483  resrhm  14558  rhmeql  14560  rhmima  14561  lmodfopne  14665  lspf  14728  znidom  14994  znrrg  14997  issubassa3  15014  innei  15266  cnovex  15299  txuni2  15359  txbasex  15360  txbas  15361  txtop  15363  txtopon  15365  txss12  15369  txbasval  15370  txcnp  15374  upxp  15375  txcnmpt  15376  uptx  15377  txcn  15378  txrest  15379  txdis  15380  cnmpt21  15394  hmeoco  15419  txhmeo  15422  isxmet2d  15451  blin2  15535  comet  15602  metcn  15617  txmetcn  15622  qtopbasss  15624  qtopbas  15625  remetdval  15650  bl2ioo  15653  blssioo  15656  divcnap  15668  cncfmet  15695  dvaddxxbr  15804  dvcjbr  15811  plyf  15840  ply1termlem  15845  plymullem1  15851  plyaddlem  15852  plymullem  15853  plycolemc  15861  plyreres  15867  dvply1  15868  efle  15879  reapef  15881  sinperlem  15912  sincosq2sgn  15931  sincosq3sgn  15932  sincos6thpi  15946  ioocosf1o  15958  reaplog  15972  relogoprlem  15973  logleb  15980  cxple3  16029  cxpcom  16046  birthdaylem2  16094  birthdaylem3  16095  dvdsppwf1o  16109  fsumdvdsmul  16111  1sgmprm  16114  mersenne  16117  pcbcctr  16123  bcmono  16124  lgslem3  16133  lgsdir2  16164  lgsdir  16166  lgsdilem2  16167  lgsdi  16168  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  gausslemma2dlem6  16198  lgseisenlem3  16203  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2  16214  lgsquad3  16215  2lgslem1a1  16217  2lgslem1a  16219  2lgslem1c  16221  2sqlem2  16246  mul2sq  16247  2sqlem7  16252  usgredg2v  16477  ushgredgedg  16479  ushgredgedgloop  16481  uhgrissubgr  16514  vtxedgfi  16542  vtxlpfi  16543  wlkeq  16607  uspgr2wlkeq  16618  clwwlkccatlem  16653  clwwlkccat  16654  clwwlknccat  16676  bj-inex  16945  bj-bdfindis  16985  triap  17090  cvgcmp2nlemabs  17093  trilpolemisumle  17099  inffz  17134