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  2247  sylan9eq  2284  csbcomg  3150  sylan9ss  3240  ssconb  3340  ineqan12d  3410  dfopg  3860  breqan12d  4104  opexg  4320  copsex2g  4338  ordin  4482  onin  4483  unexg  4540  eusv1  4549  opelvvg  4775  opthprc  4777  opbrop  4805  relop  4880  dmpropg  5209  unixpm  5272  funssres  5369  funinsn  5379  funtp  5383  fnco  5440  resasplitss  5516  fodmrnu  5567  relrnfvex  5657  funopdmsn  5834  fconst2g  5869  oveqan12d  6037  ovi3  6159  ovg  6161  f1opw2  6229  off  6248  offres  6297  iunon  6450  nnsucsssuc  6660  nnaword1  6681  ertr  6717  erex  6726  brecop  6794  ecovdi  6815  ecovidi  6816  mapvalg  6827  pmvalg  6828  pmss12g  6844  mapsn  6859  en2sn  6988  xpf1o  7030  xpen  7031  phplem4  7041  ssfilem  7062  ssfilemd  7064  diffitest  7076  en1eqsn  7147  sbthlem7  7162  ordiso  7235  updjud  7281  fodju0  7346  finnum  7387  pr2nelem  7396  djucomen  7431  exmidontriimlem1  7436  2onetap  7474  ltsopi  7540  pitric  7541  pitri3or  7542  ltdcpi  7543  mulclpi  7548  addcompig  7549  mulcompig  7551  distrpig  7553  ltexpi  7557  ltapig  7558  ltmpig  7559  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enqdc  7581  addcmpblnq  7587  addpipqqslem  7589  mulpipq2  7591  mulpipq  7592  mulpipqqs  7593  addclnq  7595  distrnqg  7607  ltdcnq  7617  ltrnqg  7640  enq0breq  7656  addclnq0  7671  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  distrnq0  7679  mulcomnq0  7680  genipv  7729  genplt2i  7730  genpelvl  7732  genpelvu  7733  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  addnqpr  7781  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  mulnqpr  7797  distrlem4prl  7804  distrlem4pru  7805  ltnqpr  7813  recexprlemloc  7851  archrecnq  7883  mulclsr  7974  1idsr  7988  00sr  7989  prsradd  8006  axmulass  8093  axdistr  8094  axcnre  8101  peano5nnnn  8112  mulrid  8176  axltadd  8249  lenlt  8255  cnegexlem3  8356  cnegex  8357  resubcl  8443  subeqrev  8555  muladd  8563  mulsub  8580  mulsub2  8581  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos2  8633  posdif  8635  addge02  8653  mullt0  8660  recexre  8758  recextlem1  8831  recexap  8833  divmuldivap  8892  conjmulap  8909  div2subap  9017  prodgt02  9033  prodge02  9035  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  ltmuldiv2  9055  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  negiso  9135  cju  9141  peano5nni  9146  nnaddcl  9163  nnmulcl  9164  nnsub  9182  addltmul  9381  avgle1  9385  avgle2  9386  nnrecl  9400  nn0nnaddcl  9433  zsubcl  9520  zleloe  9526  znnsub  9531  nzadd  9532  zmulcl  9533  zltp1le  9534  zleltp1  9535  nnleltp1  9539  nnltp1le  9540  nnaddm1cl  9541  nn0ltp1le  9542  nn0leltp1  9543  nn0ltlem1  9544  znn0sub  9545  nn0sub  9546  elz2  9551  zapne  9554  zdcle  9556  zdclt  9557  zltlen  9558  nn0lem1lt  9563  nnlem1lt  9564  nnltlem1  9565  zdiv  9568  zextle  9571  zextlt  9572  btwnnz  9574  prime  9579  nneo  9583  peano2uz2  9587  peano5uzti  9588  uzind  9591  fzind  9595  fnn0ind  9596  uzneg  9775  uz11  9779  eluzp1m1  9780  eluzp1p1  9782  uzin  9789  indstr  9827  uz2mulcl  9842  qre  9859  qaddcl  9869  qsubcl  9872  qltlen  9874  qlttri2  9875  irradd  9880  elpqb  9884  cnref1o  9885  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  rexadd  10087  rexsub  10088  xaddcom  10096  xnn0xadd0  10102  xnegdi  10103  elicc2  10173  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzval2  10246  elfz1eq  10270  peano2fzr  10272  fznlem  10276  fzsplit2  10285  fzaddel  10294  fzsubel  10295  fzrev2  10320  fzrev3  10322  uzsplit  10327  fzrevral  10340  fzrevral3  10342  fzshftral  10343  elfz2nn0  10347  fznn0sub2  10363  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  difelfznle  10370  1fv  10374  elfzouz2  10397  fzo0n  10403  fzouzsplit  10416  fzoun  10418  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  fzoaddel2  10436  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  ubmelm1fzo  10472  fzofzp1b  10474  fzosplitprm1  10481  fzostep1  10484  subfzo0  10489  zsupcllemstep  10490  qdclt  10506  qbtwnxr  10518  flqbi2  10552  divfl0  10557  flqzadd  10559  flqmulnn0  10560  addmodidr  10636  modfzo0difsn  10658  frec2uzltd  10666  frec2uzrand  10668  frecfzen2  10690  seqshft2g  10745  seq3split  10751  seqsplitg  10752  seq3caopr2  10756  seqcaopr2g  10757  seqf1oglem2  10783  exp3vallem  10803  expcllem  10813  expcl2lemap  10814  1exp  10831  expge1  10839  expadd  10844  expmul  10847  expsubap  10850  leexp1a  10857  lt2sq  10876  le2sq  10877  sumsqeq0  10881  qsqeqor  10913  bernneq  10923  bernneq2  10924  sq11ap  10970  facdiv  11001  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  facavg  11009  bcrpcl  11016  bccmpl  11017  fiubm  11093  seq3coll  11107  eqwrd  11155  ccatcl  11171  ccatclab  11172  ccatlen  11173  ccat0  11174  ccatval1  11175  ccatval2  11176  elfzelfzccat  11178  ccatvalfn  11179  ccatsymb  11180  ccatval21sw  11183  ccatrn  11187  lswccatn0lsw  11189  ccatalpha  11191  ccatrcl1  11192  swrdfv2  11245  swrdsbslen  11248  swrdspsleq  11249  swrdccat2  11253  pfxclz  11261  ccatpfx  11283  pfxccat1  11284  swrdswrdlem  11286  pfxswrd  11288  pfxccatin12lem4  11308  pfxccatin12lem1  11310  pfxccatin12lem2  11313  pfxccatin12lem3  11314  pfxccat3  11316  swrdccat  11317  pfxccatpfx2  11319  pfxccat3a  11320  swrdccat3blem  11321  swrdccat3b  11322  s2dmg  11372  shftfvalg  11380  shftf  11392  crre  11419  crim  11420  mulreap  11426  readd  11431  resub  11432  remul2  11435  imadd  11439  imsub  11440  immul2  11442  ipcnval  11448  cjsub  11454  cjreim  11465  caucvgre  11543  rexanuz  11550  rexuz3  11552  resqrexlemover  11572  resqrexlemcvg  11581  resqrexlemglsq  11584  sqrtle  11598  sqrtlt  11599  sqrt11ap  11600  sqrt11  11601  absreimsq  11629  absreim  11630  absmul  11631  sqabs  11644  absdiflt  11654  absdifle  11655  abssuble0  11665  abs2difabs  11670  fzomaxdif  11675  caubnd2  11679  rpmaxcl  11785  zmaxcl  11786  nn0maxcl  11787  minmax  11792  mincl  11793  min1inf  11794  min2inf  11795  minabs  11798  minclpr  11799  rpmincl  11800  2zinfmin  11805  xrmaxrecl  11817  xrminmax  11827  xrmincl  11828  xrmin1inf  11829  xrmin2inf  11830  xrminrecl  11835  xrminrpcl  11836  iooinsup  11839  climconst2  11853  climuni  11855  2clim  11863  climshft  11866  climshft2  11868  cjcn2  11878  climaddc1  11891  climmulc2  11893  climsubc1  11894  climsubc2  11895  climlec2  11903  summodclem2a  11944  zsumdc  11947  isumclim3  11986  mptfzshft  12005  fsumrev  12006  fisum0diag2  12010  telfsumo2  12030  fsumparts  12033  cvgcmpub  12039  binomlem  12046  binom1p  12048  binom1dif  12050  bcxmas  12052  isumshft  12053  expcnvap0  12065  expcnv  12067  geosergap  12069  geolim  12074  cvgratnnlemrate  12093  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  prodmodc  12141  zproddc  12142  fprodf1o  12151  fprodeq0  12180  efcj  12236  eftlub  12253  effsumlt  12255  efieq  12298  sinsub  12303  cossub  12304  subsin  12306  sinmul  12307  cosmul  12308  addcos  12309  subcos  12310  dvdssub2  12398  dvdsadd  12399  dvdsaddr  12400  dvdssub  12401  dvdssubr  12402  fzocongeq  12421  odd2np1  12436  opoe  12458  omoe  12459  opeo  12460  omeo  12461  divalgb  12488  ndvdsadd  12494  bitsfi  12520  gcdmndc  12528  gcdabs  12561  dvdsgcd  12585  absmulgcd  12590  gcdmultiple  12593  gcdmultiplez  12594  rpmulgcd  12599  sqgcd  12602  dvdssqlem  12603  dvdssq  12604  nninfctlemfo  12613  nn0seqcvgd  12615  ialgrlemconst  12617  algrf  12619  algrp1  12620  algcvg  12622  algcvga  12625  lcmval  12637  lcmabs  12650  lcmgcd  12652  lcmdvds  12653  lcmgcdnn  12656  coprmgcdb  12662  coprmdvds  12666  coprmdvds2  12667  qredeq  12670  isprm3  12692  nprm  12697  divgcdodd  12717  prmdvdsexp  12722  sqrt2irr  12736  zgcdsq  12775  hashdvds  12795  phiprmpw  12796  crth  12798  phimullem  12799  modprm0  12829  coprimeprodsq  12832  coprimeprodsq2  12833  pythagtriplem2  12841  pythagtriplem19  12857  pcdvdsb  12895  pcneg  12900  pc2dvds  12905  pc11  12906  pcmpt  12918  pcfac  12925  infpnlem1  12934  prmunb  12937  1arithlem4  12941  1arith  12942  gzaddcl  12952  gzmulcl  12953  gzreim  12954  gzsubcl  12955  4sqlem1  12963  4sqlem4a  12966  4sqlem4  12967  4sqlem12  12977  setsvalg  13114  setsfun0  13120  restval  13330  xpsval  13437  mndinvmod  13530  resmhm  13572  resmhm2  13573  mhmco  13575  dfgrp3m  13684  mhmmnd  13705  mulgnngsum  13716  mulgnn0z  13738  mulgnndir  13740  ghmex  13844  0ghm  13847  resghm  13849  resghm2  13850  ghmco  13853  ghmeql  13856  kerf1ghm  13863  ablsubsub23  13914  dfrhm2  14171  isrhm  14175  rhmfn  14189  rhmval  14190  rhmco  14191  resrhm  14265  rhmeql  14267  rhmima  14268  lmodfopne  14343  lspf  14406  znidom  14674  znrrg  14677  innei  14890  cnovex  14923  txuni2  14983  txbasex  14984  txbas  14985  txtop  14987  txtopon  14989  txss12  14993  txbasval  14994  txcnp  14998  upxp  14999  txcnmpt  15000  uptx  15001  txcn  15002  txrest  15003  txdis  15004  cnmpt21  15018  hmeoco  15043  txhmeo  15046  isxmet2d  15075  blin2  15159  comet  15226  metcn  15241  txmetcn  15246  qtopbasss  15248  qtopbas  15249  remetdval  15274  bl2ioo  15277  blssioo  15280  divcnap  15292  cncfmet  15319  dvaddxxbr  15428  dvcjbr  15435  plyf  15464  ply1termlem  15469  plymullem1  15475  plyaddlem  15476  plymullem  15477  plycolemc  15485  plyreres  15491  dvply1  15492  efle  15503  reapef  15505  sinperlem  15535  sincosq2sgn  15554  sincosq3sgn  15555  sincos6thpi  15569  ioocosf1o  15581  relogoprlem  15595  logleb  15602  cxple3  15648  cxpcom  15665  dvdsppwf1o  15716  fsumdvdsmul  15718  1sgmprm  15721  mersenne  15724  lgslem3  15734  lgsdir2  15765  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  gausslemma2dlem1a  15790  gausslemma2dlem3  15795  gausslemma2dlem6  15799  lgseisenlem3  15804  lgseisenlem4  15805  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2  15815  lgsquad3  15816  2lgslem1a1  15818  2lgslem1a  15820  2lgslem1c  15822  2sqlem2  15847  mul2sq  15848  2sqlem7  15853  usgredg2v  16078  ushgredgedg  16080  ushgredgedgloop  16082  uhgrissubgr  16115  vtxedgfi  16143  vtxlpfi  16144  wlkeq  16208  uspgr2wlkeq  16219  clwwlkccatlem  16254  clwwlkccat  16255  clwwlknccat  16277  bj-inex  16523  bj-bdfindis  16563  triap  16654  cvgcmp2nlemabs  16657  trilpolemisumle  16663  inffz  16697