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  596  syl2an2r  597  orandc  945  mp3an3an  1377  eqeqan12d  2245  sylan9eq  2282  csbcomg  3147  sylan9ss  3237  ssconb  3337  ineqan12d  3407  dfopg  3855  breqan12d  4099  opexg  4314  copsex2g  4332  ordin  4476  onin  4477  unexg  4534  eusv1  4543  opelvvg  4768  opthprc  4770  opbrop  4798  relop  4872  dmpropg  5201  unixpm  5264  funssres  5360  funinsn  5370  funtp  5374  fnco  5431  resasplitss  5507  fodmrnu  5558  relrnfvex  5647  funopdmsn  5823  fconst2g  5858  oveqan12d  6026  ovi3  6148  ovg  6150  f1opw2  6218  off  6237  offres  6286  iunon  6436  nnsucsssuc  6646  nnaword1  6667  ertr  6703  erex  6712  brecop  6780  ecovdi  6801  ecovidi  6802  mapvalg  6813  pmvalg  6814  pmss12g  6830  mapsn  6845  en2sn  6974  xpf1o  7013  xpen  7014  phplem4  7024  ssfilem  7045  diffitest  7057  en1eqsn  7123  sbthlem7  7138  ordiso  7211  updjud  7257  fodju0  7322  finnum  7363  pr2nelem  7372  djucomen  7406  exmidontriimlem1  7411  2onetap  7449  ltsopi  7515  pitric  7516  pitri3or  7517  ltdcpi  7518  mulclpi  7523  addcompig  7524  mulcompig  7526  distrpig  7528  ltexpi  7532  ltapig  7533  ltmpig  7534  dfplpq2  7549  dfmpq2  7550  enqbreq2  7552  enqdc  7556  addcmpblnq  7562  addpipqqslem  7564  mulpipq2  7566  mulpipq  7567  mulpipqqs  7568  addclnq  7570  distrnqg  7582  ltdcnq  7592  ltrnqg  7615  enq0breq  7631  addclnq0  7646  nqnq0a  7649  nqnq0m  7650  nq0m0r  7651  distrnq0  7654  mulcomnq0  7655  genipv  7704  genplt2i  7705  genpelvl  7707  genpelvu  7708  addnqprlemrl  7752  addnqprlemru  7753  addnqprlemfl  7754  addnqprlemfu  7755  addnqpr  7756  mulnqprlemrl  7768  mulnqprlemru  7769  mulnqprlemfl  7770  mulnqprlemfu  7771  mulnqpr  7772  distrlem4prl  7779  distrlem4pru  7780  ltnqpr  7788  recexprlemloc  7826  archrecnq  7858  mulclsr  7949  1idsr  7963  00sr  7964  prsradd  7981  axmulass  8068  axdistr  8069  axcnre  8076  peano5nnnn  8087  mulrid  8151  axltadd  8224  lenlt  8230  cnegexlem3  8331  cnegex  8332  resubcl  8418  subeqrev  8530  muladd  8538  mulsub  8555  mulsub2  8556  ltaddsub2  8592  leaddsub2  8594  leltadd  8602  ltaddpos2  8608  posdif  8610  addge02  8628  mullt0  8635  recexre  8733  recextlem1  8806  recexap  8808  divmuldivap  8867  conjmulap  8884  div2subap  8992  prodgt02  9008  prodge02  9010  lemul2  9012  lemul2a  9014  ltmulgt12  9020  lemulge12  9022  ltmuldiv2  9030  ltdivmul2  9033  ledivmul2  9035  lemuldiv2  9037  negiso  9110  cju  9116  peano5nni  9121  nnaddcl  9138  nnmulcl  9139  nnsub  9157  addltmul  9356  avgle1  9360  avgle2  9361  nnrecl  9375  nn0nnaddcl  9408  zsubcl  9495  zleloe  9501  znnsub  9506  nzadd  9507  zmulcl  9508  zltp1le  9509  zleltp1  9510  nnleltp1  9514  nnltp1le  9515  nnaddm1cl  9516  nn0ltp1le  9517  nn0leltp1  9518  nn0ltlem1  9519  znn0sub  9520  nn0sub  9521  elz2  9526  zapne  9529  zdcle  9531  zdclt  9532  zltlen  9533  nn0lem1lt  9538  nnlem1lt  9539  nnltlem1  9540  zdiv  9543  zextle  9546  zextlt  9547  btwnnz  9549  prime  9554  nneo  9558  peano2uz2  9562  peano5uzti  9563  uzind  9566  fzind  9570  fnn0ind  9571  uzneg  9749  uz11  9753  eluzp1m1  9754  eluzp1p1  9756  uzin  9763  indstr  9796  uz2mulcl  9811  qre  9828  qaddcl  9838  qsubcl  9841  qltlen  9843  qlttri2  9844  irradd  9849  elpqb  9853  cnref1o  9854  rpaddcl  9881  rpmulcl  9882  rpdivcl  9883  rexadd  10056  rexsub  10057  xaddcom  10065  xnn0xadd0  10071  xnegdi  10072  elicc2  10142  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  fzval2  10215  elfz1eq  10239  peano2fzr  10241  fznlem  10245  fzsplit2  10254  fzaddel  10263  fzsubel  10264  fzrev2  10289  fzrev3  10291  uzsplit  10296  fzrevral  10309  fzrevral3  10311  fzshftral  10312  elfz2nn0  10316  fznn0sub2  10332  fz0fzdiffz0  10334  elfzmlbp  10336  difelfzle  10338  difelfznle  10339  1fv  10343  elfzouz2  10366  fzo0n  10372  fzouzsplit  10385  fzoun  10387  elfzo0le  10393  fzonmapblen  10395  fzofzim  10396  fzoaddel2  10404  eluzgtdifelfzo  10411  elfzodifsumelfzo  10415  ubmelm1fzo  10440  fzofzp1b  10442  fzosplitprm1  10448  fzostep1  10451  subfzo0  10456  zsupcllemstep  10457  qdclt  10473  qbtwnxr  10485  flqbi2  10519  divfl0  10524  flqzadd  10526  flqmulnn0  10527  addmodidr  10603  modfzo0difsn  10625  frec2uzltd  10633  frec2uzrand  10635  frecfzen2  10657  seqshft2g  10712  seq3split  10718  seqsplitg  10719  seq3caopr2  10723  seqcaopr2g  10724  seqf1oglem2  10750  exp3vallem  10770  expcllem  10780  expcl2lemap  10781  1exp  10798  expge1  10806  expadd  10811  expmul  10814  expsubap  10817  leexp1a  10824  lt2sq  10843  le2sq  10844  sumsqeq0  10848  qsqeqor  10880  bernneq  10890  bernneq2  10891  sq11ap  10937  facdiv  10968  faclbnd  10971  faclbnd3  10973  faclbnd6  10974  facavg  10976  bcrpcl  10983  bccmpl  10984  fiubm  11058  seq3coll  11072  eqwrd  11120  ccatcl  11136  ccatclab  11137  ccatlen  11138  ccat0  11139  ccatval1  11140  ccatval2  11141  elfzelfzccat  11143  ccatvalfn  11144  ccatsymb  11145  ccatval21sw  11148  ccatrn  11152  lswccatn0lsw  11154  swrdfv2  11203  swrdsbslen  11206  swrdspsleq  11207  swrdccat2  11211  pfxclz  11219  ccatpfx  11241  pfxccat1  11242  swrdswrdlem  11244  pfxswrd  11246  pfxccatin12lem4  11266  pfxccatin12lem1  11268  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccat3  11274  swrdccat  11275  pfxccatpfx2  11277  pfxccat3a  11278  swrdccat3blem  11279  swrdccat3b  11280  s2dmg  11330  shftfvalg  11337  shftf  11349  crre  11376  crim  11377  mulreap  11383  readd  11388  resub  11389  remul2  11392  imadd  11396  imsub  11397  immul2  11399  ipcnval  11405  cjsub  11411  cjreim  11422  caucvgre  11500  rexanuz  11507  rexuz3  11509  resqrexlemover  11529  resqrexlemcvg  11538  resqrexlemglsq  11541  sqrtle  11555  sqrtlt  11556  sqrt11ap  11557  sqrt11  11558  absreimsq  11586  absreim  11587  absmul  11588  sqabs  11601  absdiflt  11611  absdifle  11612  abssuble0  11622  abs2difabs  11627  fzomaxdif  11632  caubnd2  11636  rpmaxcl  11742  zmaxcl  11743  nn0maxcl  11744  minmax  11749  mincl  11750  min1inf  11751  min2inf  11752  minabs  11755  minclpr  11756  rpmincl  11757  2zinfmin  11762  xrmaxrecl  11774  xrminmax  11784  xrmincl  11785  xrmin1inf  11786  xrmin2inf  11787  xrminrecl  11792  xrminrpcl  11793  iooinsup  11796  climconst2  11810  climuni  11812  2clim  11820  climshft  11823  climshft2  11825  cjcn2  11835  climaddc1  11848  climmulc2  11850  climsubc1  11851  climsubc2  11852  climlec2  11860  summodclem2a  11900  zsumdc  11903  isumclim3  11942  mptfzshft  11961  fsumrev  11962  fisum0diag2  11966  telfsumo2  11986  fsumparts  11989  cvgcmpub  11995  binomlem  12002  binom1p  12004  binom1dif  12006  bcxmas  12008  isumshft  12009  expcnvap0  12021  expcnv  12023  geosergap  12025  geolim  12030  cvgratnnlemrate  12049  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  prodmodc  12097  zproddc  12098  fprodf1o  12107  fprodeq0  12136  efcj  12192  eftlub  12209  effsumlt  12211  efieq  12254  sinsub  12259  cossub  12260  subsin  12262  sinmul  12263  cosmul  12264  addcos  12265  subcos  12266  dvdssub2  12354  dvdsadd  12355  dvdsaddr  12356  dvdssub  12357  dvdssubr  12358  fzocongeq  12377  odd2np1  12392  opoe  12414  omoe  12415  opeo  12416  omeo  12417  divalgb  12444  ndvdsadd  12450  bitsfi  12476  gcdmndc  12484  gcdabs  12517  dvdsgcd  12541  absmulgcd  12546  gcdmultiple  12549  gcdmultiplez  12550  rpmulgcd  12555  sqgcd  12558  dvdssqlem  12559  dvdssq  12560  nninfctlemfo  12569  nn0seqcvgd  12571  ialgrlemconst  12573  algrf  12575  algrp1  12576  algcvg  12578  algcvga  12581  lcmval  12593  lcmabs  12606  lcmgcd  12608  lcmdvds  12609  lcmgcdnn  12612  coprmgcdb  12618  coprmdvds  12622  coprmdvds2  12623  qredeq  12626  isprm3  12648  nprm  12653  divgcdodd  12673  prmdvdsexp  12678  sqrt2irr  12692  zgcdsq  12731  hashdvds  12751  phiprmpw  12752  crth  12754  phimullem  12755  modprm0  12785  coprimeprodsq  12788  coprimeprodsq2  12789  pythagtriplem2  12797  pythagtriplem19  12813  pcdvdsb  12851  pcneg  12856  pc2dvds  12861  pc11  12862  pcmpt  12874  pcfac  12881  infpnlem1  12890  prmunb  12893  1arithlem4  12897  1arith  12898  gzaddcl  12908  gzmulcl  12909  gzreim  12910  gzsubcl  12911  4sqlem1  12919  4sqlem4a  12922  4sqlem4  12923  4sqlem12  12933  setsvalg  13070  setsfun0  13076  restval  13286  xpsval  13393  mndinvmod  13486  resmhm  13528  resmhm2  13529  mhmco  13531  dfgrp3m  13640  mhmmnd  13661  mulgnngsum  13672  mulgnn0z  13694  mulgnndir  13696  ghmex  13800  0ghm  13803  resghm  13805  resghm2  13806  ghmco  13809  ghmeql  13812  kerf1ghm  13819  ablsubsub23  13870  dfrhm2  14126  isrhm  14130  rhmfn  14144  rhmval  14145  rhmco  14146  resrhm  14220  rhmeql  14222  rhmima  14223  lmodfopne  14298  lspf  14361  znidom  14629  znrrg  14632  innei  14845  cnovex  14878  txuni2  14938  txbasex  14939  txbas  14940  txtop  14942  txtopon  14944  txss12  14948  txbasval  14949  txcnp  14953  upxp  14954  txcnmpt  14955  uptx  14956  txcn  14957  txrest  14958  txdis  14959  cnmpt21  14973  hmeoco  14998  txhmeo  15001  isxmet2d  15030  blin2  15114  comet  15181  metcn  15196  txmetcn  15201  qtopbasss  15203  qtopbas  15204  remetdval  15229  bl2ioo  15232  blssioo  15235  divcnap  15247  cncfmet  15274  dvaddxxbr  15383  dvcjbr  15390  plyf  15419  ply1termlem  15424  plymullem1  15430  plyaddlem  15431  plymullem  15432  plycolemc  15440  plyreres  15446  dvply1  15447  efle  15458  reapef  15460  sinperlem  15490  sincosq2sgn  15509  sincosq3sgn  15510  sincos6thpi  15524  ioocosf1o  15536  relogoprlem  15550  logleb  15557  cxple3  15603  cxpcom  15620  dvdsppwf1o  15671  fsumdvdsmul  15673  1sgmprm  15676  mersenne  15679  lgslem3  15689  lgsdir2  15720  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  gausslemma2dlem6  15754  lgseisenlem3  15759  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2  15770  lgsquad3  15771  2lgslem1a1  15773  2lgslem1a  15775  2lgslem1c  15777  2sqlem2  15802  mul2sq  15803  2sqlem7  15808  usgredg2v  16030  ushgredgedg  16032  ushgredgedgloop  16034  wlkeq  16075  uspgr2wlkeq  16086  bj-inex  16294  bj-bdfindis  16334  triap  16427  cvgcmp2nlemabs  16430  trilpolemisumle  16436  inffz  16470