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  602  syl2an2r  603  orandc  952  mp3an3an  1384  eqeqan12d  2254  sylan9eq  2291  csbcomg  3170  sylan9ss  3261  ssconb  3362  ineqan12d  3434  dfopg  3900  breqan12d  4144  opexg  4366  copsex2g  4384  ordin  4528  onin  4529  unexg  4587  eusv1  4596  opelvvg  4822  opthprc  4824  opbrop  4852  relop  4928  dmpropg  5258  unixpm  5321  funssres  5418  funinsn  5428  funtp  5432  fnco  5489  resasplitss  5567  fodmrnu  5621  relrnfvex  5711  funopdmsn  5889  fconst2g  5924  oveqan12d  6098  ovi3  6220  ovg  6222  f1opw2  6290  off  6309  offres  6362  suppfnss  6491  iunon  6549  nnsucsssuc  6759  nnaword1  6780  ertr  6816  erex  6825  brecop  6893  ecovdi  6914  ecovidi  6915  mapvalg  6926  pmvalg  6927  pmss12g  6950  mapsn  6966  en2sn  7096  xpf1o  7138  xpen  7139  phplem4  7150  ssfilem  7171  ssfilemd  7173  diffitest  7185  en1eqsn  7259  sbthlem7  7274  fsuppxpfi  7290  ordiso  7370  updjud  7416  fodju0  7481  finnum  7522  pr2nelem  7531  djucomen  7566  exmidontriimlem1  7571  2onetap  7615  ltsopi  7681  pitric  7682  pitri3or  7683  ltdcpi  7684  mulclpi  7689  addcompig  7690  mulcompig  7692  distrpig  7694  ltexpi  7698  ltapig  7699  ltmpig  7700  dfplpq2  7715  dfmpq2  7716  enqbreq2  7718  enqdc  7722  addcmpblnq  7728  addpipqqslem  7730  mulpipq2  7732  mulpipq  7733  mulpipqqs  7734  addclnq  7736  distrnqg  7748  ltdcnq  7758  ltrnqg  7781  enq0breq  7797  addclnq0  7812  nqnq0a  7815  nqnq0m  7816  nq0m0r  7817  distrnq0  7820  mulcomnq0  7821  genipv  7870  genplt2i  7871  genpelvl  7873  genpelvu  7874  addnqprlemrl  7918  addnqprlemru  7919  addnqprlemfl  7920  addnqprlemfu  7921  addnqpr  7922  mulnqprlemrl  7934  mulnqprlemru  7935  mulnqprlemfl  7936  mulnqprlemfu  7937  mulnqpr  7938  distrlem4prl  7945  distrlem4pru  7946  ltnqpr  7954  recexprlemloc  7992  archrecnq  8024  mulclsr  8115  1idsr  8129  00sr  8130  prsradd  8147  axmulass  8234  axdistr  8235  axcnre  8242  peano5nnnn  8253  mulrid  8317  axltadd  8389  lenlt  8395  cnegexlem3  8497  cnegex  8498  resubcl  8584  subeqrev  8696  muladd  8705  mulsub  8722  mulsub2  8723  ltaddsub2  8759  leaddsub2  8761  leltadd  8769  ltaddpos2  8775  posdif  8777  addge02  8795  mullt0  8802  recexre  8900  recextlem1  8973  recexap  8975  divmuldivap  9036  conjmulap  9053  div2subap  9161  prodgt02  9177  prodge02  9179  lemul2  9181  lemul2a  9183  ltmulgt12  9189  lemulge12  9191  ltmuldiv2  9199  ltdivmul2  9202  ledivmul2  9204  lemuldiv2  9206  negiso  9279  cju  9285  peano5nni  9290  nnaddcl  9307  nnmulcl  9308  nnsub  9326  addltmul  9525  avgle1  9529  avgle2  9530  nnrecl  9544  nn0nnaddcl  9577  zsubcl  9668  zleloe  9674  znnsub  9679  nzadd  9680  zmulcl  9681  zltp1le  9682  zleltp1  9683  nnleltp1  9687  nnltp1le  9688  nnaddm1cl  9689  nn0ltp1le  9690  nn0leltp1  9691  nn0ltlem1  9692  znn0sub  9693  nn0sub  9694  elz2  9699  zapne  9702  zdcle  9704  zdclt  9705  zltlen  9707  nn0lem1lt  9712  nnlem1lt  9713  nnltlem1  9714  zdiv  9717  zextle  9720  zextlt  9721  btwnnz  9723  prime  9728  nneo  9732  peano2uz2  9736  peano5uzti  9737  uzind  9740  fzind  9744  fnn0ind  9745  uzneg  9924  uz11  9928  eluzp1m1  9929  eluzp1p1  9931  uzin  9938  indstr  9976  uz2mulcl  9991  qre  10008  qaddcl  10018  qsubcl  10021  qltlen  10023  qlttri2  10024  irradd  10029  elpqb  10033  cnref1o  10034  rpaddcl  10061  rpmulcl  10062  rpdivcl  10063  rexadd  10237  rexsub  10238  xaddcom  10246  xnn0xadd0  10252  xnegdi  10253  elicc2  10323  iccshftr  10379  iccshftl  10381  iccdil  10383  icccntr  10385  fzval2  10397  elfz1eq  10422  peano2fzr  10424  fznlem  10428  fzsplit2  10438  fzsplit3  10441  fzaddel  10448  fzsubel  10449  fzrev2  10475  fzrev3  10477  uzsplit  10482  fzrevral  10495  fzrevral3  10497  fzshftral  10498  elfz2nn0  10502  fznn0sub2  10518  fz0fzdiffz0  10520  elfzmlbp  10522  difelfzle  10524  difelfznle  10525  1fv  10529  elfzouz2  10552  fzo0n  10558  fzouzsplit  10571  fzoun  10573  elfzo0le  10580  fzonmapblen  10582  fzofzim  10583  fzoaddel2  10591  eluzgtdifelfzo  10598  elfzodifsumelfzo  10602  ubmelm1fzo  10627  fzofzp1b  10629  fzosplitprm1  10636  fzostep1  10639  subfzo0  10644  zsupcllemstep  10645  qdclt  10663  qbtwnxr  10675  flqbi2  10709  divfl0  10714  flqzadd  10716  flqmulnn0  10717  addmodidr  10793  modfzo0difsn  10815  frec2uzltd  10823  frec2uzrand  10825  frecfzen2  10847  seqshft2g  10902  seq3split  10908  seqsplitg  10909  seq3caopr2  10913  seqcaopr2g  10914  seqf1oglem2  10940  exp3vallem  10960  expcllem  10970  expcl2lemap  10971  1exp  10988  expge1  10996  expadd  11001  expmul  11004  expsubap  11007  leexp1a  11014  lt2sq  11033  le2sq  11034  sumsqeq0  11038  qsqeqor  11070  bernneq  11081  bernneq2  11082  sq11ap  11128  facdiv  11159  faclbnd  11162  faclbnd3  11164  faclbnd6  11165  facavg  11167  bcrpcl  11174  bccmpl  11175  bcm1n  11190  fiubm  11254  seq3coll  11277  eqwrd  11328  ccatcl  11344  ccatclab  11345  ccatlen  11346  ccat0  11347  ccatval1  11348  ccatval2  11349  elfzelfzccat  11351  ccatvalfn  11352  ccatsymb  11353  ccatval21sw  11356  ccatrn  11360  lswccatn0lsw  11362  ccatalpha  11364  ccatrcl1  11365  swrdfv2  11418  swrdsbslen  11421  swrdspsleq  11422  swrdccat2  11426  pfxclz  11434  ccatpfx  11456  pfxccat1  11457  swrdswrdlem  11459  pfxswrd  11461  pfxccatin12lem4  11481  pfxccatin12lem1  11483  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccat3  11489  swrdccat  11490  pfxccatpfx2  11492  pfxccat3a  11493  swrdccat3blem  11494  swrdccat3b  11495  s2dmg  11545  shftfvalg  11566  shftf  11578  crre  11605  crim  11606  mulreap  11612  readd  11617  resub  11618  remul2  11621  imadd  11625  imsub  11626  immul2  11628  ipcnval  11634  cjsub  11640  cjreim  11652  caucvgre  11730  rexanuz  11737  rexuz3  11739  resqrexlemover  11759  resqrexlemcvg  11768  resqrexlemglsq  11771  sqrtle  11785  sqrtlt  11786  sqrt11ap  11787  sqrt11  11788  absreimsq  11816  absreim  11817  absmul  11818  sqabs  11831  absdiflt  11841  absdifle  11842  abssuble0  11852  abs2difabs  11857  fzomaxdif  11862  caubnd2  11866  rpmaxcl  11972  zmaxcl  11973  nn0maxcl  11974  minmax  11979  mincl  11980  min1inf  11981  min2inf  11982  minabs  11985  minclpr  11986  rpmincl  11987  2zinfmin  11992  xrmaxrecl  12004  xrminmax  12014  xrmincl  12015  xrmin1inf  12016  xrmin2inf  12017  xrminrecl  12022  xrminrpcl  12023  iooinsup  12026  climconst2  12040  climuni  12042  2clim  12050  climshft  12053  climshft2  12055  cjcn2  12065  climaddc1  12078  climmulc2  12080  climsubc1  12081  climsubc2  12082  climlec2  12090  summodclem2a  12131  zsumdc  12134  isumclim3  12173  mptfzshft  12192  fsumrev  12193  fisum0diag2  12197  telfsumo2  12217  fsumparts  12220  cvgcmpub  12226  binomlem  12233  binom1p  12235  binom1dif  12237  bcxmas  12239  isumshft  12240  expcnvap0  12252  expcnv  12254  geosergap  12256  geolim  12261  cvgratnnlemrate  12280  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  prodmodc  12328  zproddc  12329  fprodf1o  12338  fprodeq0  12367  efcj  12423  eftlub  12440  effsumlt  12442  efieq  12485  sinsub  12490  cossub  12491  subsin  12493  sinmul  12494  cosmul  12495  addcos  12496  subcos  12497  dvdssub2  12585  dvdsadd  12586  dvdsaddr  12587  dvdssub  12588  dvdssubr  12589  fzocongeq  12608  odd2np1  12623  opoe  12645  omoe  12646  opeo  12647  omeo  12648  divalgb  12675  ndvdsadd  12681  bitsfi  12707  gcdmndc  12715  gcdabs  12748  dvdsgcd  12772  absmulgcd  12777  gcdmultiple  12780  gcdmultiplez  12781  rpmulgcd  12786  sqgcd  12789  dvdssqlem  12790  dvdssq  12791  nninfctlemfo  12800  nn0seqcvgd  12802  ialgrlemconst  12804  algrf  12806  algrp1  12807  algcvg  12809  algcvga  12812  lcmval  12824  lcmabs  12837  lcmgcd  12839  lcmdvds  12840  lcmgcdnn  12843  coprmgcdb  12849  coprmdvds  12853  coprmdvds2  12854  qredeq  12857  isprm3  12879  nprm  12884  divgcdodd  12904  prmdvdsexp  12909  sqrt2irr  12923  zgcdsq  12962  hashdvds  12982  phiprmpw  12983  crth  12985  phimullem  12986  modprm0  13016  coprimeprodsq  13019  coprimeprodsq2  13020  pythagtriplem2  13028  pythagtriplem19  13044  pcdvdsb  13082  pcneg  13087  pc2dvds  13092  pc11  13093  pcmpt  13105  pcfac  13112  infpnlem1  13121  prmunb  13124  1arithlem4  13128  1arith  13129  gzaddcl  13139  gzmulcl  13140  gzreim  13141  gzsubcl  13142  4sqlem1  13150  4sqlem4a  13153  4sqlem4  13154  4sqlem12  13164  ballotfilemfc0  13215  ballotfilemfcc  13216  setsvalg  13365  setsfun0  13371  restval  13582  mndinvmod  13741  resmhm  13777  resmhm2  13778  mhmco  13780  dfgrp3m  13887  mhmmnd  13902  mulgnngzsum  13913  mulgnn0z  13935  mulgnndir  13937  ghmex  14041  0ghm  14044  resghm  14046  resghm2  14047  ghmco  14050  ghmeql  14053  kerf1ghm  14060  ablsubsub23  14112  xpsval  14184  dfrhm2  14444  isrhm  14448  rhmfn  14462  rhmval  14463  rhmco  14464  resrhm  14539  rhmeql  14541  rhmima  14542  lmodfopne  14646  lspf  14709  znidom  14975  znrrg  14978  issubassa3  14995  innei  15247  cnovex  15280  txuni2  15340  txbasex  15341  txbas  15342  txtop  15344  txtopon  15346  txss12  15350  txbasval  15351  txcnp  15355  upxp  15356  txcnmpt  15357  uptx  15358  txcn  15359  txrest  15360  txdis  15361  cnmpt21  15375  hmeoco  15400  txhmeo  15403  isxmet2d  15432  blin2  15516  comet  15583  metcn  15598  txmetcn  15603  qtopbasss  15605  qtopbas  15606  remetdval  15631  bl2ioo  15634  blssioo  15637  divcnap  15649  cncfmet  15676  dvaddxxbr  15785  dvcjbr  15792  plyf  15821  ply1termlem  15826  plymullem1  15832  plyaddlem  15833  plymullem  15834  plycolemc  15842  plyreres  15848  dvply1  15849  efle  15860  reapef  15862  sinperlem  15892  sincosq2sgn  15911  sincosq3sgn  15912  sincos6thpi  15926  ioocosf1o  15938  relogoprlem  15952  logleb  15959  cxple3  16006  cxpcom  16023  birthdaylem2  16071  birthdaylem3  16072  dvdsppwf1o  16086  fsumdvdsmul  16088  1sgmprm  16091  mersenne  16094  lgslem3  16104  lgsdir2  16135  lgsdir  16137  lgsdilem2  16138  lgsdi  16139  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  gausslemma2dlem6  16169  lgseisenlem3  16174  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2  16185  lgsquad3  16186  2lgslem1a1  16188  2lgslem1a  16190  2lgslem1c  16192  2sqlem2  16217  mul2sq  16218  2sqlem7  16223  usgredg2v  16448  ushgredgedg  16450  ushgredgedgloop  16452  uhgrissubgr  16485  vtxedgfi  16513  vtxlpfi  16514  wlkeq  16578  uspgr2wlkeq  16589  clwwlkccatlem  16624  clwwlkccat  16625  clwwlknccat  16647  bj-inex  16916  bj-bdfindis  16956  triap  17052  cvgcmp2nlemabs  17055  trilpolemisumle  17061  inffz  17096