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 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  syl2anr  290  anim12i  338  syl2an2  598  syl2an2r  599  orandc  947  mp3an3an  1379  eqeqan12d  2246  sylan9eq  2283  csbcomg  3149  sylan9ss  3239  ssconb  3339  ineqan12d  3409  dfopg  3861  breqan12d  4105  opexg  4322  copsex2g  4340  ordin  4484  onin  4485  unexg  4542  eusv1  4551  opelvvg  4777  opthprc  4779  opbrop  4807  relop  4882  dmpropg  5211  unixpm  5274  funssres  5371  funinsn  5381  funtp  5385  fnco  5442  resasplitss  5518  fodmrnu  5570  relrnfvex  5660  funopdmsn  5837  fconst2g  5872  oveqan12d  6042  ovi3  6164  ovg  6166  f1opw2  6234  off  6253  offres  6302  iunon  6455  nnsucsssuc  6665  nnaword1  6686  ertr  6722  erex  6731  brecop  6799  ecovdi  6820  ecovidi  6821  mapvalg  6832  pmvalg  6833  pmss12g  6849  mapsn  6864  en2sn  6993  xpf1o  7035  xpen  7036  phplem4  7046  ssfilem  7067  ssfilemd  7069  diffitest  7081  en1eqsn  7152  sbthlem7  7167  ordiso  7240  updjud  7286  fodju0  7351  finnum  7392  pr2nelem  7401  djucomen  7436  exmidontriimlem1  7441  2onetap  7479  ltsopi  7545  pitric  7546  pitri3or  7547  ltdcpi  7548  mulclpi  7553  addcompig  7554  mulcompig  7556  distrpig  7558  ltexpi  7562  ltapig  7563  ltmpig  7564  dfplpq2  7579  dfmpq2  7580  enqbreq2  7582  enqdc  7586  addcmpblnq  7592  addpipqqslem  7594  mulpipq2  7596  mulpipq  7597  mulpipqqs  7598  addclnq  7600  distrnqg  7612  ltdcnq  7622  ltrnqg  7645  enq0breq  7661  addclnq0  7676  nqnq0a  7679  nqnq0m  7680  nq0m0r  7681  distrnq0  7684  mulcomnq0  7685  genipv  7734  genplt2i  7735  genpelvl  7737  genpelvu  7738  addnqprlemrl  7782  addnqprlemru  7783  addnqprlemfl  7784  addnqprlemfu  7785  addnqpr  7786  mulnqprlemrl  7798  mulnqprlemru  7799  mulnqprlemfl  7800  mulnqprlemfu  7801  mulnqpr  7802  distrlem4prl  7809  distrlem4pru  7810  ltnqpr  7818  recexprlemloc  7856  archrecnq  7888  mulclsr  7979  1idsr  7993  00sr  7994  prsradd  8011  axmulass  8098  axdistr  8099  axcnre  8106  peano5nnnn  8117  mulrid  8181  axltadd  8254  lenlt  8260  cnegexlem3  8361  cnegex  8362  resubcl  8448  subeqrev  8560  muladd  8568  mulsub  8585  mulsub2  8586  ltaddsub2  8622  leaddsub2  8624  leltadd  8632  ltaddpos2  8638  posdif  8640  addge02  8658  mullt0  8665  recexre  8763  recextlem1  8836  recexap  8838  divmuldivap  8897  conjmulap  8914  div2subap  9022  prodgt02  9038  prodge02  9040  lemul2  9042  lemul2a  9044  ltmulgt12  9050  lemulge12  9052  ltmuldiv2  9060  ltdivmul2  9063  ledivmul2  9065  lemuldiv2  9067  negiso  9140  cju  9146  peano5nni  9151  nnaddcl  9168  nnmulcl  9169  nnsub  9187  addltmul  9386  avgle1  9390  avgle2  9391  nnrecl  9405  nn0nnaddcl  9438  zsubcl  9525  zleloe  9531  znnsub  9536  nzadd  9537  zmulcl  9538  zltp1le  9539  zleltp1  9540  nnleltp1  9544  nnltp1le  9545  nnaddm1cl  9546  nn0ltp1le  9547  nn0leltp1  9548  nn0ltlem1  9549  znn0sub  9550  nn0sub  9551  elz2  9556  zapne  9559  zdcle  9561  zdclt  9562  zltlen  9563  nn0lem1lt  9568  nnlem1lt  9569  nnltlem1  9570  zdiv  9573  zextle  9576  zextlt  9577  btwnnz  9579  prime  9584  nneo  9588  peano2uz2  9592  peano5uzti  9593  uzind  9596  fzind  9600  fnn0ind  9601  uzneg  9780  uz11  9784  eluzp1m1  9785  eluzp1p1  9787  uzin  9794  indstr  9832  uz2mulcl  9847  qre  9864  qaddcl  9874  qsubcl  9877  qltlen  9879  qlttri2  9880  irradd  9885  elpqb  9889  cnref1o  9890  rpaddcl  9917  rpmulcl  9918  rpdivcl  9919  rexadd  10092  rexsub  10093  xaddcom  10101  xnn0xadd0  10107  xnegdi  10108  elicc2  10178  iccshftr  10234  iccshftl  10236  iccdil  10238  icccntr  10240  fzval2  10251  elfz1eq  10275  peano2fzr  10277  fznlem  10281  fzsplit2  10290  fzaddel  10299  fzsubel  10300  fzrev2  10325  fzrev3  10327  uzsplit  10332  fzrevral  10345  fzrevral3  10347  fzshftral  10348  elfz2nn0  10352  fznn0sub2  10368  fz0fzdiffz0  10370  elfzmlbp  10372  difelfzle  10374  difelfznle  10375  1fv  10379  elfzouz2  10402  fzo0n  10408  fzouzsplit  10421  fzoun  10423  elfzo0le  10430  fzonmapblen  10432  fzofzim  10433  fzoaddel2  10441  eluzgtdifelfzo  10448  elfzodifsumelfzo  10452  ubmelm1fzo  10477  fzofzp1b  10479  fzosplitprm1  10486  fzostep1  10489  subfzo0  10494  zsupcllemstep  10495  qdclt  10511  qbtwnxr  10523  flqbi2  10557  divfl0  10562  flqzadd  10564  flqmulnn0  10565  addmodidr  10641  modfzo0difsn  10663  frec2uzltd  10671  frec2uzrand  10673  frecfzen2  10695  seqshft2g  10750  seq3split  10756  seqsplitg  10757  seq3caopr2  10761  seqcaopr2g  10762  seqf1oglem2  10788  exp3vallem  10808  expcllem  10818  expcl2lemap  10819  1exp  10836  expge1  10844  expadd  10849  expmul  10852  expsubap  10855  leexp1a  10862  lt2sq  10881  le2sq  10882  sumsqeq0  10886  qsqeqor  10918  bernneq  10928  bernneq2  10929  sq11ap  10975  facdiv  11006  faclbnd  11009  faclbnd3  11011  faclbnd6  11012  facavg  11014  bcrpcl  11021  bccmpl  11022  fiubm  11098  seq3coll  11112  eqwrd  11163  ccatcl  11179  ccatclab  11180  ccatlen  11181  ccat0  11182  ccatval1  11183  ccatval2  11184  elfzelfzccat  11186  ccatvalfn  11187  ccatsymb  11188  ccatval21sw  11191  ccatrn  11195  lswccatn0lsw  11197  ccatalpha  11199  ccatrcl1  11200  swrdfv2  11253  swrdsbslen  11256  swrdspsleq  11257  swrdccat2  11261  pfxclz  11269  ccatpfx  11291  pfxccat1  11292  swrdswrdlem  11294  pfxswrd  11296  pfxccatin12lem4  11316  pfxccatin12lem1  11318  pfxccatin12lem2  11321  pfxccatin12lem3  11322  pfxccat3  11324  swrdccat  11325  pfxccatpfx2  11327  pfxccat3a  11328  swrdccat3blem  11329  swrdccat3b  11330  s2dmg  11380  shftfvalg  11401  shftf  11413  crre  11440  crim  11441  mulreap  11447  readd  11452  resub  11453  remul2  11456  imadd  11460  imsub  11461  immul2  11463  ipcnval  11469  cjsub  11475  cjreim  11486  caucvgre  11564  rexanuz  11571  rexuz3  11573  resqrexlemover  11593  resqrexlemcvg  11602  resqrexlemglsq  11605  sqrtle  11619  sqrtlt  11620  sqrt11ap  11621  sqrt11  11622  absreimsq  11650  absreim  11651  absmul  11652  sqabs  11665  absdiflt  11675  absdifle  11676  abssuble0  11686  abs2difabs  11691  fzomaxdif  11696  caubnd2  11700  rpmaxcl  11806  zmaxcl  11807  nn0maxcl  11808  minmax  11813  mincl  11814  min1inf  11815  min2inf  11816  minabs  11819  minclpr  11820  rpmincl  11821  2zinfmin  11826  xrmaxrecl  11838  xrminmax  11848  xrmincl  11849  xrmin1inf  11850  xrmin2inf  11851  xrminrecl  11856  xrminrpcl  11857  iooinsup  11860  climconst2  11874  climuni  11876  2clim  11884  climshft  11887  climshft2  11889  cjcn2  11899  climaddc1  11912  climmulc2  11914  climsubc1  11915  climsubc2  11916  climlec2  11924  summodclem2a  11965  zsumdc  11968  isumclim3  12007  mptfzshft  12026  fsumrev  12027  fisum0diag2  12031  telfsumo2  12051  fsumparts  12054  cvgcmpub  12060  binomlem  12067  binom1p  12069  binom1dif  12071  bcxmas  12073  isumshft  12074  expcnvap0  12086  expcnv  12088  geosergap  12090  geolim  12095  cvgratnnlemrate  12114  mertenslemi1  12119  mertenslem2  12120  mertensabs  12121  prodmodc  12162  zproddc  12163  fprodf1o  12172  fprodeq0  12201  efcj  12257  eftlub  12274  effsumlt  12276  efieq  12319  sinsub  12324  cossub  12325  subsin  12327  sinmul  12328  cosmul  12329  addcos  12330  subcos  12331  dvdssub2  12419  dvdsadd  12420  dvdsaddr  12421  dvdssub  12422  dvdssubr  12423  fzocongeq  12442  odd2np1  12457  opoe  12479  omoe  12480  opeo  12481  omeo  12482  divalgb  12509  ndvdsadd  12515  bitsfi  12541  gcdmndc  12549  gcdabs  12582  dvdsgcd  12606  absmulgcd  12611  gcdmultiple  12614  gcdmultiplez  12615  rpmulgcd  12620  sqgcd  12623  dvdssqlem  12624  dvdssq  12625  nninfctlemfo  12634  nn0seqcvgd  12636  ialgrlemconst  12638  algrf  12640  algrp1  12641  algcvg  12643  algcvga  12646  lcmval  12658  lcmabs  12671  lcmgcd  12673  lcmdvds  12674  lcmgcdnn  12677  coprmgcdb  12683  coprmdvds  12687  coprmdvds2  12688  qredeq  12691  isprm3  12713  nprm  12718  divgcdodd  12738  prmdvdsexp  12743  sqrt2irr  12757  zgcdsq  12796  hashdvds  12816  phiprmpw  12817  crth  12819  phimullem  12820  modprm0  12850  coprimeprodsq  12853  coprimeprodsq2  12854  pythagtriplem2  12862  pythagtriplem19  12878  pcdvdsb  12916  pcneg  12921  pc2dvds  12926  pc11  12927  pcmpt  12939  pcfac  12946  infpnlem1  12955  prmunb  12958  1arithlem4  12962  1arith  12963  gzaddcl  12973  gzmulcl  12974  gzreim  12975  gzsubcl  12976  4sqlem1  12984  4sqlem4a  12987  4sqlem4  12988  4sqlem12  12998  setsvalg  13135  setsfun0  13141  restval  13351  xpsval  13458  mndinvmod  13551  resmhm  13593  resmhm2  13594  mhmco  13596  dfgrp3m  13705  mhmmnd  13726  mulgnngsum  13737  mulgnn0z  13759  mulgnndir  13761  ghmex  13865  0ghm  13868  resghm  13870  resghm2  13871  ghmco  13874  ghmeql  13877  kerf1ghm  13884  ablsubsub23  13935  dfrhm2  14192  isrhm  14196  rhmfn  14210  rhmval  14211  rhmco  14212  resrhm  14286  rhmeql  14288  rhmima  14289  lmodfopne  14364  lspf  14427  znidom  14695  znrrg  14698  innei  14916  cnovex  14949  txuni2  15009  txbasex  15010  txbas  15011  txtop  15013  txtopon  15015  txss12  15019  txbasval  15020  txcnp  15024  upxp  15025  txcnmpt  15026  uptx  15027  txcn  15028  txrest  15029  txdis  15030  cnmpt21  15044  hmeoco  15069  txhmeo  15072  isxmet2d  15101  blin2  15185  comet  15252  metcn  15267  txmetcn  15272  qtopbasss  15274  qtopbas  15275  remetdval  15300  bl2ioo  15303  blssioo  15306  divcnap  15318  cncfmet  15345  dvaddxxbr  15454  dvcjbr  15461  plyf  15490  ply1termlem  15495  plymullem1  15501  plyaddlem  15502  plymullem  15503  plycolemc  15511  plyreres  15517  dvply1  15518  efle  15529  reapef  15531  sinperlem  15561  sincosq2sgn  15580  sincosq3sgn  15581  sincos6thpi  15595  ioocosf1o  15607  relogoprlem  15621  logleb  15628  cxple3  15674  cxpcom  15691  dvdsppwf1o  15742  fsumdvdsmul  15744  1sgmprm  15747  mersenne  15750  lgslem3  15760  lgsdir2  15791  lgsdir  15793  lgsdilem2  15794  lgsdi  15795  gausslemma2dlem1a  15816  gausslemma2dlem3  15821  gausslemma2dlem6  15825  lgseisenlem3  15830  lgseisenlem4  15831  lgsquadlem1  15835  lgsquadlem2  15836  lgsquad2  15841  lgsquad3  15842  2lgslem1a1  15844  2lgslem1a  15846  2lgslem1c  15848  2sqlem2  15873  mul2sq  15874  2sqlem7  15879  usgredg2v  16104  ushgredgedg  16106  ushgredgedgloop  16108  uhgrissubgr  16141  vtxedgfi  16169  vtxlpfi  16170  wlkeq  16234  uspgr2wlkeq  16245  clwwlkccatlem  16280  clwwlkccat  16281  clwwlknccat  16303  bj-inex  16562  bj-bdfindis  16602  triap  16700  cvgcmp2nlemabs  16703  trilpolemisumle  16709  inffz  16744