Theorem syl2an 283

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 277	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 280	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  syl2anr  284  anim12i  331  syl2an2  558  syl2an2r  559  mp3an3an  1274  eqeqan12d  2096  sylan9eq  2133  csbcomg  2929  sylan9ss  3012  ssconb  3105  ineqan12d  3169  dfopg  3568  breqan12d  3800  opexg  3983  copsex2g  4001  ordin  4140  onin  4141  unexg  4196  eusv1  4202  opelvvg  4407  opthprc  4409  opbrop  4437  relop  4504  dmpropg  4813  unixpm  4873  funssres  4962  funtp  4972  fnco  5027  resasplitss  5089  fodmrnu  5134  relrnfvex  5213  fconst2g  5397  oveqan12d  5551  ovi3  5657  ovg  5659  f1opw2  5726  off  5744  offres  5782  iunon  5922  nnsucsssuc  6094  nnaword1  6109  ertr  6144  erex  6153  brecop  6219  ecovdi  6240  ecovidi  6241  en2sn  6313  phplem4  6341  ssfilem  6360  diffitest  6371  ordiso  6447  finnum  6452  pr2nelem  6460  ltsopi  6510  pitric  6511  pitri3or  6512  ltdcpi  6513  mulclpi  6518  addcompig  6519  mulcompig  6521  distrpig  6523  ltexpi  6527  ltapig  6528  ltmpig  6529  dfplpq2  6544  dfmpq2  6545  enqbreq2  6547  enqdc  6551  addcmpblnq  6557  addpipqqslem  6559  mulpipq2  6561  mulpipq  6562  mulpipqqs  6563  addclnq  6565  distrnqg  6577  ltdcnq  6587  ltrnqg  6610  enq0breq  6626  addclnq0  6641  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  distrnq0  6649  mulcomnq0  6650  genipv  6699  genplt2i  6700  genpelvl  6702  genpelvu  6703  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  addnqpr  6751  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  mulnqpr  6767  distrlem4prl  6774  distrlem4pru  6775  ltnqpr  6783  recexprlemloc  6821  archrecnq  6853  mulclsr  6931  1idsr  6945  00sr  6946  prsradd  6962  axmulass  7039  axdistr  7040  axcnre  7047  peano5nnnn  7058  mulid1  7116  axltadd  7182  lenlt  7187  cnegexlem3  7285  cnegex  7286  resubcl  7372  subeqrev  7480  muladd  7488  mulsub  7505  mulsub2  7506  ltaddsub2  7541  leaddsub2  7543  leltadd  7551  ltaddpos2  7557  posdif  7559  addge02  7577  mullt0  7584  recexre  7678  recextlem1  7741  recexap  7743  divmuldivap  7800  conjmulap  7817  prodgt02  7931  prodge02  7933  lemul2  7935  lemul2a  7937  ltmulgt12  7943  lemulge12  7945  ltmuldiv2  7953  ltdivmul2  7956  ledivmul2  7958  lemuldiv2  7960  negiso  8033  cju  8038  peano5nni  8042  nnaddcl  8059  nnmulcl  8060  nnsub  8077  addltmul  8267  avgle1  8271  avgle2  8272  nnrecl  8286  nn0nnaddcl  8319  zsubcl  8392  zleloe  8398  znnsub  8402  nzadd  8403  zmulcl  8404  zltp1le  8405  zleltp1  8406  nnleltp1  8410  nnltp1le  8411  nnaddm1cl  8412  nn0ltp1le  8413  nn0leltp1  8414  nn0ltlem1  8415  znn0sub  8416  nn0sub  8417  elz2  8419  zapne  8422  zdcle  8424  zdclt  8425  zltlen  8426  nn0lem1lt  8430  nnlem1lt  8431  nnltlem1  8432  zdiv  8435  zextle  8438  zextlt  8439  btwnnz  8441  prime  8446  nneo  8450  peano2uz2  8454  peano5uzti  8455  uzind  8458  fzind  8462  fnn0ind  8463  uzneg  8637  uz11  8641  eluzp1m1  8642  eluzp1p1  8644  uzin  8651  indstr  8681  uz2mulcl  8695  qre  8710  qaddcl  8720  qsubcl  8723  qltlen  8725  qlttri2  8726  irradd  8731  cnref1o  8733  rpaddcl  8757  rpmulcl  8758  rpdivcl  8759  elicc2  8961  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzval2  9032  elfz1eq  9054  peano2fzr  9056  fznlem  9060  fzsplit2  9069  fzaddel  9077  fzsubel  9078  fzrev2  9102  fzrev3  9104  uzsplit  9109  fzrevral  9122  fzrevral3  9124  fzshftral  9125  elfz2nn0  9128  fznn0sub2  9139  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  difelfznle  9146  1fv  9149  elfzouz2  9170  fzouzsplit  9188  elfzo0le  9194  fzonmapblen  9196  fzofzim  9197  fzoaddel2  9202  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  ubmelm1fzo  9235  fzofzp1b  9237  fzosplitprm1  9243  fzostep1  9246  subfzo0  9251  qbtwnxr  9266  flqbi2  9293  divfl0  9298  flqzadd  9300  flqmulnn0  9301  addmodidr  9375  modfzo0difsn  9397  frec2uzltd  9405  frec2uzrand  9407  frecfzen2  9420  iseqshft2  9452  iseqsplit  9458  iseqcaopr2  9461  expcllem  9487  expcl2lemap  9488  1exp  9505  expge1  9513  expadd  9518  expmul  9521  expsubap  9524  leexp1a  9531  lt2sq  9549  le2sq  9550  sumsqeq0  9554  bernneq  9593  bernneq2  9594  sq11ap  9639  facdiv  9665  faclbnd  9668  faclbnd3  9670  faclbnd6  9671  facavg  9673  bcrpcl  9680  bccmpl  9681  shftfvalg  9706  shftf  9718  crre  9744  crim  9745  mulreap  9751  readd  9756  resub  9757  remul2  9760  imadd  9764  imsub  9765  immul2  9767  ipcnval  9773  cjsub  9779  cjreim  9790  caucvgre  9867  rexanuz  9874  rexuz3  9876  resqrexlemover  9896  resqrexlemcvg  9905  resqrexlemglsq  9908  sqrtle  9922  sqrtlt  9923  sqrt11ap  9924  sqrt11  9925  absreimsq  9953  absreim  9954  absmul  9955  sqabs  9968  absdiflt  9978  absdifle  9979  abssuble0  9989  abs2difabs  9994  fzomaxdif  9999  caubnd2  10003  minmax  10112  min1inf  10113  min2inf  10114  climconst2  10130  climuni  10132  2clim  10140  climshft  10143  climshft2  10145  cjcn2  10154  climaddc1  10167  climmulc2  10169  climsubc1  10170  climsubc2  10171  climlec2  10179  dvdssub2  10237  dvdsadd  10238  dvdsaddr  10239  dvdssub  10240  dvdssubr  10241  fzocongeq  10258  odd2np1  10272  opoe  10295  omoe  10296  opeo  10297  omeo  10298  divalgb  10325  ndvdsadd  10331  zsupcllemstep  10341  gcdabs  10379  dvdsgcd  10401  absmulgcd  10406  gcdmultiple  10409  gcdmultiplez  10410  rpmulgcd  10415  sqgcd  10418  dvdssqlem  10419  dvdssq  10420  nn0seqcvgd  10423  ialgrlemconst  10425  ialgrp1  10428  ialgcvg  10430  ialgcvga  10433  lcmval  10445  lcmabs  10458  lcmgcd  10460  lcmdvds  10461  lcmgcdnn  10464  coprmgcdb  10470  coprmdvds  10474  coprmdvds2  10475  qredeq  10478  isprm3  10500  nprm  10505  divgcdodd  10522  prmdvdsexp  10527  sqrt2irr  10541  bj-inex  10698  bj-bdfindis  10742