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  594  syl2an2r  595  orandc  941  mp3an3an  1354  eqeqan12d  2212  sylan9eq  2249  csbcomg  3107  sylan9ss  3197  ssconb  3297  ineqan12d  3367  dfopg  3807  breqan12d  4050  opexg  4262  copsex2g  4280  ordin  4421  onin  4422  unexg  4479  eusv1  4488  opelvvg  4713  opthprc  4715  opbrop  4743  relop  4817  dmpropg  5143  unixpm  5206  funssres  5301  funinsn  5308  funtp  5312  fnco  5369  resasplitss  5440  fodmrnu  5491  relrnfvex  5579  fconst2g  5780  oveqan12d  5944  ovi3  6064  ovg  6066  f1opw2  6133  off  6152  offres  6201  iunon  6351  nnsucsssuc  6559  nnaword1  6580  ertr  6616  erex  6625  brecop  6693  ecovdi  6714  ecovidi  6715  mapvalg  6726  pmvalg  6727  pmss12g  6743  mapsn  6758  en2sn  6881  xpf1o  6914  xpen  6915  phplem4  6925  ssfilem  6945  diffitest  6957  en1eqsn  7023  sbthlem7  7038  ordiso  7111  updjud  7157  fodju0  7222  finnum  7263  pr2nelem  7272  djucomen  7301  exmidontriimlem1  7306  2onetap  7340  ltsopi  7406  pitric  7407  pitri3or  7408  ltdcpi  7409  mulclpi  7414  addcompig  7415  mulcompig  7417  distrpig  7419  ltexpi  7423  ltapig  7424  ltmpig  7425  dfplpq2  7440  dfmpq2  7441  enqbreq2  7443  enqdc  7447  addcmpblnq  7453  addpipqqslem  7455  mulpipq2  7457  mulpipq  7458  mulpipqqs  7459  addclnq  7461  distrnqg  7473  ltdcnq  7483  ltrnqg  7506  enq0breq  7522  addclnq0  7537  nqnq0a  7540  nqnq0m  7541  nq0m0r  7542  distrnq0  7545  mulcomnq0  7546  genipv  7595  genplt2i  7596  genpelvl  7598  genpelvu  7599  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  addnqpr  7647  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  mulnqpr  7663  distrlem4prl  7670  distrlem4pru  7671  ltnqpr  7679  recexprlemloc  7717  archrecnq  7749  mulclsr  7840  1idsr  7854  00sr  7855  prsradd  7872  axmulass  7959  axdistr  7960  axcnre  7967  peano5nnnn  7978  mulrid  8042  axltadd  8115  lenlt  8121  cnegexlem3  8222  cnegex  8223  resubcl  8309  subeqrev  8421  muladd  8429  mulsub  8446  mulsub2  8447  ltaddsub2  8483  leaddsub2  8485  leltadd  8493  ltaddpos2  8499  posdif  8501  addge02  8519  mullt0  8526  recexre  8624  recextlem1  8697  recexap  8699  divmuldivap  8758  conjmulap  8775  div2subap  8883  prodgt02  8899  prodge02  8901  lemul2  8903  lemul2a  8905  ltmulgt12  8911  lemulge12  8913  ltmuldiv2  8921  ltdivmul2  8924  ledivmul2  8926  lemuldiv2  8928  negiso  9001  cju  9007  peano5nni  9012  nnaddcl  9029  nnmulcl  9030  nnsub  9048  addltmul  9247  avgle1  9251  avgle2  9252  nnrecl  9266  nn0nnaddcl  9299  zsubcl  9386  zleloe  9392  znnsub  9396  nzadd  9397  zmulcl  9398  zltp1le  9399  zleltp1  9400  nnleltp1  9404  nnltp1le  9405  nnaddm1cl  9406  nn0ltp1le  9407  nn0leltp1  9408  nn0ltlem1  9409  znn0sub  9410  nn0sub  9411  elz2  9416  zapne  9419  zdcle  9421  zdclt  9422  zltlen  9423  nn0lem1lt  9428  nnlem1lt  9429  nnltlem1  9430  zdiv  9433  zextle  9436  zextlt  9437  btwnnz  9439  prime  9444  nneo  9448  peano2uz2  9452  peano5uzti  9453  uzind  9456  fzind  9460  fnn0ind  9461  uzneg  9639  uz11  9643  eluzp1m1  9644  eluzp1p1  9646  uzin  9653  indstr  9686  uz2mulcl  9701  qre  9718  qaddcl  9728  qsubcl  9731  qltlen  9733  qlttri2  9734  irradd  9739  elpqb  9743  cnref1o  9744  rpaddcl  9771  rpmulcl  9772  rpdivcl  9773  rexadd  9946  rexsub  9947  xaddcom  9955  xnn0xadd0  9961  xnegdi  9962  elicc2  10032  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzval2  10105  elfz1eq  10129  peano2fzr  10131  fznlem  10135  fzsplit2  10144  fzaddel  10153  fzsubel  10154  fzrev2  10179  fzrev3  10181  uzsplit  10186  fzrevral  10199  fzrevral3  10201  fzshftral  10202  elfz2nn0  10206  fznn0sub2  10222  fz0fzdiffz0  10224  elfzmlbp  10226  difelfzle  10228  difelfznle  10229  1fv  10233  elfzouz2  10256  fzouzsplit  10274  elfzo0le  10280  fzonmapblen  10282  fzofzim  10283  fzoaddel2  10288  eluzgtdifelfzo  10292  elfzodifsumelfzo  10296  ubmelm1fzo  10321  fzofzp1b  10323  fzosplitprm1  10329  fzostep1  10332  subfzo0  10337  zsupcllemstep  10338  qdclt  10354  qbtwnxr  10366  flqbi2  10400  divfl0  10405  flqzadd  10407  flqmulnn0  10408  addmodidr  10484  modfzo0difsn  10506  frec2uzltd  10514  frec2uzrand  10516  frecfzen2  10538  seqshft2g  10593  seq3split  10599  seqsplitg  10600  seq3caopr2  10604  seqcaopr2g  10605  seqf1oglem2  10631  exp3vallem  10651  expcllem  10661  expcl2lemap  10662  1exp  10679  expge1  10687  expadd  10692  expmul  10695  expsubap  10698  leexp1a  10705  lt2sq  10724  le2sq  10725  sumsqeq0  10729  qsqeqor  10761  bernneq  10771  bernneq2  10772  sq11ap  10818  facdiv  10849  faclbnd  10852  faclbnd3  10854  faclbnd6  10855  facavg  10857  bcrpcl  10864  bccmpl  10865  fiubm  10939  seq3coll  10953  eqwrd  10994  shftfvalg  11002  shftf  11014  crre  11041  crim  11042  mulreap  11048  readd  11053  resub  11054  remul2  11057  imadd  11061  imsub  11062  immul2  11064  ipcnval  11070  cjsub  11076  cjreim  11087  caucvgre  11165  rexanuz  11172  rexuz3  11174  resqrexlemover  11194  resqrexlemcvg  11203  resqrexlemglsq  11206  sqrtle  11220  sqrtlt  11221  sqrt11ap  11222  sqrt11  11223  absreimsq  11251  absreim  11252  absmul  11253  sqabs  11266  absdiflt  11276  absdifle  11277  abssuble0  11287  abs2difabs  11292  fzomaxdif  11297  caubnd2  11301  rpmaxcl  11407  zmaxcl  11408  nn0maxcl  11409  minmax  11414  mincl  11415  min1inf  11416  min2inf  11417  minabs  11420  minclpr  11421  rpmincl  11422  2zinfmin  11427  xrmaxrecl  11439  xrminmax  11449  xrmincl  11450  xrmin1inf  11451  xrmin2inf  11452  xrminrecl  11457  xrminrpcl  11458  iooinsup  11461  climconst2  11475  climuni  11477  2clim  11485  climshft  11488  climshft2  11490  cjcn2  11500  climaddc1  11513  climmulc2  11515  climsubc1  11516  climsubc2  11517  climlec2  11525  summodclem2a  11565  zsumdc  11568  isumclim3  11607  mptfzshft  11626  fsumrev  11627  fisum0diag2  11631  telfsumo2  11651  fsumparts  11654  cvgcmpub  11660  binomlem  11667  binom1p  11669  binom1dif  11671  bcxmas  11673  isumshft  11674  expcnvap0  11686  expcnv  11688  geosergap  11690  geolim  11695  cvgratnnlemrate  11714  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodeq0  11801  efcj  11857  eftlub  11874  effsumlt  11876  efieq  11919  sinsub  11924  cossub  11925  subsin  11927  sinmul  11928  cosmul  11929  addcos  11930  subcos  11931  dvdssub2  12019  dvdsadd  12020  dvdsaddr  12021  dvdssub  12022  dvdssubr  12023  fzocongeq  12042  odd2np1  12057  opoe  12079  omoe  12080  opeo  12081  omeo  12082  divalgb  12109  ndvdsadd  12115  bitsfi  12141  gcdmndc  12149  gcdabs  12182  dvdsgcd  12206  absmulgcd  12211  gcdmultiple  12214  gcdmultiplez  12215  rpmulgcd  12220  sqgcd  12223  dvdssqlem  12224  dvdssq  12225  nninfctlemfo  12234  nn0seqcvgd  12236  ialgrlemconst  12238  algrf  12240  algrp1  12241  algcvg  12243  algcvga  12246  lcmval  12258  lcmabs  12271  lcmgcd  12273  lcmdvds  12274  lcmgcdnn  12277  coprmgcdb  12283  coprmdvds  12287  coprmdvds2  12288  qredeq  12291  isprm3  12313  nprm  12318  divgcdodd  12338  prmdvdsexp  12343  sqrt2irr  12357  zgcdsq  12396  hashdvds  12416  phiprmpw  12417  crth  12419  phimullem  12420  modprm0  12450  coprimeprodsq  12453  coprimeprodsq2  12454  pythagtriplem2  12462  pythagtriplem19  12478  pcdvdsb  12516  pcneg  12521  pc2dvds  12526  pc11  12527  pcmpt  12539  pcfac  12546  infpnlem1  12555  prmunb  12558  1arithlem4  12562  1arith  12563  gzaddcl  12573  gzmulcl  12574  gzreim  12575  gzsubcl  12576  4sqlem1  12584  4sqlem4a  12587  4sqlem4  12588  4sqlem12  12598  setsvalg  12735  setsfun0  12741  restval  12949  xpsval  13056  mndinvmod  13149  resmhm  13191  resmhm2  13192  mhmco  13194  dfgrp3m  13303  mhmmnd  13324  mulgnngsum  13335  mulgnn0z  13357  mulgnndir  13359  ghmex  13463  0ghm  13466  resghm  13468  resghm2  13469  ghmco  13472  ghmeql  13475  kerf1ghm  13482  ablsubsub23  13533  dfrhm2  13788  isrhm  13792  rhmfn  13806  rhmval  13807  rhmco  13808  resrhm  13882  rhmeql  13884  rhmima  13885  lmodfopne  13960  lspf  14023  znidom  14291  znrrg  14294  innei  14485  cnovex  14518  txuni2  14578  txbasex  14579  txbas  14580  txtop  14582  txtopon  14584  txss12  14588  txbasval  14589  txcnp  14593  upxp  14594  txcnmpt  14595  uptx  14596  txcn  14597  txrest  14598  txdis  14599  cnmpt21  14613  hmeoco  14638  txhmeo  14641  isxmet2d  14670  blin2  14754  comet  14821  metcn  14836  txmetcn  14841  qtopbasss  14843  qtopbas  14844  remetdval  14869  bl2ioo  14872  blssioo  14875  divcnap  14887  cncfmet  14914  dvaddxxbr  15023  dvcjbr  15030  plyf  15059  ply1termlem  15064  plymullem1  15070  plyaddlem  15071  plymullem  15072  plycolemc  15080  plyreres  15086  dvply1  15087  efle  15098  reapef  15100  sinperlem  15130  sincosq2sgn  15149  sincosq3sgn  15150  sincos6thpi  15164  ioocosf1o  15176  relogoprlem  15190  logleb  15197  cxple3  15243  cxpcom  15260  dvdsppwf1o  15311  fsumdvdsmul  15313  1sgmprm  15316  mersenne  15319  lgslem3  15329  lgsdir2  15360  lgsdir  15362  lgsdilem2  15363  lgsdi  15364  gausslemma2dlem1a  15385  gausslemma2dlem3  15390  gausslemma2dlem6  15394  lgseisenlem3  15399  lgseisenlem4  15400  lgsquadlem1  15404  lgsquadlem2  15405  lgsquad2  15410  lgsquad3  15411  2lgslem1a1  15413  2lgslem1a  15415  2lgslem1c  15417  2sqlem2  15442  mul2sq  15443  2sqlem7  15448  bj-inex  15639  bj-bdfindis  15679  triap  15764  cvgcmp2nlemabs  15767  trilpolemisumle  15773  inffz  15807