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  2209  sylan9eq  2246  csbcomg  3104  sylan9ss  3193  ssconb  3293  ineqan12d  3363  dfopg  3803  breqan12d  4046  opexg  4258  copsex2g  4276  ordin  4417  onin  4418  unexg  4475  eusv1  4484  opelvvg  4709  opthprc  4711  opbrop  4739  relop  4813  dmpropg  5139  unixpm  5202  funssres  5297  funinsn  5304  funtp  5308  fnco  5363  resasplitss  5434  fodmrnu  5485  relrnfvex  5573  fconst2g  5774  oveqan12d  5938  ovi3  6057  ovg  6059  f1opw2  6126  off  6145  offres  6189  iunon  6339  nnsucsssuc  6547  nnaword1  6568  ertr  6604  erex  6613  brecop  6681  ecovdi  6702  ecovidi  6703  mapvalg  6714  pmvalg  6715  pmss12g  6731  mapsn  6746  en2sn  6869  xpf1o  6902  xpen  6903  phplem4  6913  ssfilem  6933  diffitest  6945  en1eqsn  7009  sbthlem7  7024  ordiso  7097  updjud  7143  fodju0  7208  finnum  7245  pr2nelem  7253  djucomen  7278  exmidontriimlem1  7283  2onetap  7317  ltsopi  7382  pitric  7383  pitri3or  7384  ltdcpi  7385  mulclpi  7390  addcompig  7391  mulcompig  7393  distrpig  7395  ltexpi  7399  ltapig  7400  ltmpig  7401  dfplpq2  7416  dfmpq2  7417  enqbreq2  7419  enqdc  7423  addcmpblnq  7429  addpipqqslem  7431  mulpipq2  7433  mulpipq  7434  mulpipqqs  7435  addclnq  7437  distrnqg  7449  ltdcnq  7459  ltrnqg  7482  enq0breq  7498  addclnq0  7513  nqnq0a  7516  nqnq0m  7517  nq0m0r  7518  distrnq0  7521  mulcomnq0  7522  genipv  7571  genplt2i  7572  genpelvl  7574  genpelvu  7575  addnqprlemrl  7619  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  addnqpr  7623  mulnqprlemrl  7635  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  mulnqpr  7639  distrlem4prl  7646  distrlem4pru  7647  ltnqpr  7655  recexprlemloc  7693  archrecnq  7725  mulclsr  7816  1idsr  7830  00sr  7831  prsradd  7848  axmulass  7935  axdistr  7936  axcnre  7943  peano5nnnn  7954  mulrid  8018  axltadd  8091  lenlt  8097  cnegexlem3  8198  cnegex  8199  resubcl  8285  subeqrev  8397  muladd  8405  mulsub  8422  mulsub2  8423  ltaddsub2  8458  leaddsub2  8460  leltadd  8468  ltaddpos2  8474  posdif  8476  addge02  8494  mullt0  8501  recexre  8599  recextlem1  8672  recexap  8674  divmuldivap  8733  conjmulap  8750  div2subap  8858  prodgt02  8874  prodge02  8876  lemul2  8878  lemul2a  8880  ltmulgt12  8886  lemulge12  8888  ltmuldiv2  8896  ltdivmul2  8899  ledivmul2  8901  lemuldiv2  8903  negiso  8976  cju  8982  peano5nni  8987  nnaddcl  9004  nnmulcl  9005  nnsub  9023  addltmul  9222  avgle1  9226  avgle2  9227  nnrecl  9241  nn0nnaddcl  9274  zsubcl  9361  zleloe  9367  znnsub  9371  nzadd  9372  zmulcl  9373  zltp1le  9374  zleltp1  9375  nnleltp1  9379  nnltp1le  9380  nnaddm1cl  9381  nn0ltp1le  9382  nn0leltp1  9383  nn0ltlem1  9384  znn0sub  9385  nn0sub  9386  elz2  9391  zapne  9394  zdcle  9396  zdclt  9397  zltlen  9398  nn0lem1lt  9403  nnlem1lt  9404  nnltlem1  9405  zdiv  9408  zextle  9411  zextlt  9412  btwnnz  9414  prime  9419  nneo  9423  peano2uz2  9427  peano5uzti  9428  uzind  9431  fzind  9435  fnn0ind  9436  uzneg  9614  uz11  9618  eluzp1m1  9619  eluzp1p1  9621  uzin  9628  indstr  9661  uz2mulcl  9676  qre  9693  qaddcl  9703  qsubcl  9706  qltlen  9708  qlttri2  9709  irradd  9714  elpqb  9718  cnref1o  9719  rpaddcl  9746  rpmulcl  9747  rpdivcl  9748  rexadd  9921  rexsub  9922  xaddcom  9930  xnn0xadd0  9936  xnegdi  9937  elicc2  10007  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzval2  10080  elfz1eq  10104  peano2fzr  10106  fznlem  10110  fzsplit2  10119  fzaddel  10128  fzsubel  10129  fzrev2  10154  fzrev3  10156  uzsplit  10161  fzrevral  10174  fzrevral3  10176  fzshftral  10177  elfz2nn0  10181  fznn0sub2  10197  fz0fzdiffz0  10199  elfzmlbp  10201  difelfzle  10203  difelfznle  10204  1fv  10208  elfzouz2  10231  fzouzsplit  10249  elfzo0le  10255  fzonmapblen  10257  fzofzim  10258  fzoaddel2  10263  eluzgtdifelfzo  10267  elfzodifsumelfzo  10271  ubmelm1fzo  10296  fzofzp1b  10298  fzosplitprm1  10304  fzostep1  10307  subfzo0  10312  qdclt  10318  qbtwnxr  10329  flqbi2  10363  divfl0  10368  flqzadd  10370  flqmulnn0  10371  addmodidr  10447  modfzo0difsn  10469  frec2uzltd  10477  frec2uzrand  10479  frecfzen2  10501  seqshft2g  10556  seq3split  10562  seqsplitg  10563  seq3caopr2  10567  seqcaopr2g  10568  seqf1oglem2  10594  exp3vallem  10614  expcllem  10624  expcl2lemap  10625  1exp  10642  expge1  10650  expadd  10655  expmul  10658  expsubap  10661  leexp1a  10668  lt2sq  10687  le2sq  10688  sumsqeq0  10692  qsqeqor  10724  bernneq  10734  bernneq2  10735  sq11ap  10781  facdiv  10812  faclbnd  10815  faclbnd3  10817  faclbnd6  10818  facavg  10820  bcrpcl  10827  bccmpl  10828  fiubm  10902  seq3coll  10916  eqwrd  10957  shftfvalg  10965  shftf  10977  crre  11004  crim  11005  mulreap  11011  readd  11016  resub  11017  remul2  11020  imadd  11024  imsub  11025  immul2  11027  ipcnval  11033  cjsub  11039  cjreim  11050  caucvgre  11128  rexanuz  11135  rexuz3  11137  resqrexlemover  11157  resqrexlemcvg  11166  resqrexlemglsq  11169  sqrtle  11183  sqrtlt  11184  sqrt11ap  11185  sqrt11  11186  absreimsq  11214  absreim  11215  absmul  11216  sqabs  11229  absdiflt  11239  absdifle  11240  abssuble0  11250  abs2difabs  11255  fzomaxdif  11260  caubnd2  11264  rpmaxcl  11370  zmaxcl  11371  minmax  11376  mincl  11377  min1inf  11378  min2inf  11379  minabs  11382  minclpr  11383  rpmincl  11384  2zinfmin  11389  xrmaxrecl  11401  xrminmax  11411  xrmincl  11412  xrmin1inf  11413  xrmin2inf  11414  xrminrecl  11419  xrminrpcl  11420  iooinsup  11423  climconst2  11437  climuni  11439  2clim  11447  climshft  11450  climshft2  11452  cjcn2  11462  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  climlec2  11487  summodclem2a  11527  zsumdc  11530  isumclim3  11569  mptfzshft  11588  fsumrev  11589  fisum0diag2  11593  telfsumo2  11613  fsumparts  11616  cvgcmpub  11622  binomlem  11629  binom1p  11631  binom1dif  11633  bcxmas  11635  isumshft  11636  expcnvap0  11648  expcnv  11650  geosergap  11652  geolim  11657  cvgratnnlemrate  11676  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodmodc  11724  zproddc  11725  fprodf1o  11734  fprodeq0  11763  efcj  11819  eftlub  11836  effsumlt  11838  efieq  11881  sinsub  11886  cossub  11887  subsin  11889  sinmul  11890  cosmul  11891  addcos  11892  subcos  11893  dvdssub2  11981  dvdsadd  11982  dvdsaddr  11983  dvdssub  11984  dvdssubr  11985  fzocongeq  12003  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  divalgb  12069  ndvdsadd  12075  gcdmndc  12084  zsupcllemstep  12085  gcdabs  12128  dvdsgcd  12152  absmulgcd  12157  gcdmultiple  12160  gcdmultiplez  12161  rpmulgcd  12166  sqgcd  12169  dvdssqlem  12170  dvdssq  12171  nninfctlemfo  12180  nn0seqcvgd  12182  ialgrlemconst  12184  algrf  12186  algrp1  12187  algcvg  12189  algcvga  12192  lcmval  12204  lcmabs  12217  lcmgcd  12219  lcmdvds  12220  lcmgcdnn  12223  coprmgcdb  12229  coprmdvds  12233  coprmdvds2  12234  qredeq  12237  isprm3  12259  nprm  12264  divgcdodd  12284  prmdvdsexp  12289  sqrt2irr  12303  zgcdsq  12342  hashdvds  12362  phiprmpw  12363  crth  12365  phimullem  12366  modprm0  12395  coprimeprodsq  12398  coprimeprodsq2  12399  pythagtriplem2  12407  pythagtriplem19  12423  pcdvdsb  12461  pcneg  12466  pc2dvds  12471  pc11  12472  pcmpt  12484  pcfac  12491  infpnlem1  12500  prmunb  12503  1arithlem4  12507  1arith  12508  gzaddcl  12518  gzmulcl  12519  gzreim  12520  gzsubcl  12521  4sqlem1  12529  4sqlem4a  12532  4sqlem4  12533  4sqlem12  12543  setsvalg  12651  setsfun0  12657  restval  12859  xpsval  12938  mndinvmod  13029  resmhm  13062  resmhm2  13063  mhmco  13065  dfgrp3m  13174  mhmmnd  13189  mulgnngsum  13200  mulgnn0z  13222  mulgnndir  13224  ghmex  13328  0ghm  13331  resghm  13333  resghm2  13334  ghmco  13337  ghmeql  13340  kerf1ghm  13347  ablsubsub23  13398  dfrhm2  13653  isrhm  13657  rhmfn  13671  rhmval  13672  rhmco  13673  resrhm  13747  rhmeql  13749  rhmima  13750  lmodfopne  13825  lspf  13888  znidom  14156  znrrg  14159  innei  14342  cnovex  14375  txuni2  14435  txbasex  14436  txbas  14437  txtop  14439  txtopon  14441  txss12  14445  txbasval  14446  txcnp  14450  upxp  14451  txcnmpt  14452  uptx  14453  txcn  14454  txrest  14455  txdis  14456  cnmpt21  14470  hmeoco  14495  txhmeo  14498  isxmet2d  14527  blin2  14611  comet  14678  metcn  14693  txmetcn  14698  qtopbasss  14700  qtopbas  14701  remetdval  14726  bl2ioo  14729  blssioo  14732  divcnap  14744  cncfmet  14771  dvaddxxbr  14880  dvcjbr  14887  plyf  14916  ply1termlem  14921  plymullem1  14927  plyaddlem  14928  plymullem  14929  plycolemc  14936  plyreres  14942  dvply1  14943  efle  14952  reapef  14954  sinperlem  14984  sincosq2sgn  15003  sincosq3sgn  15004  sincos6thpi  15018  ioocosf1o  15030  relogoprlem  15044  logleb  15051  cxple3  15096  cxpcom  15112  lgslem3  15159  lgsdir2  15190  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  gausslemma2dlem6  15224  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2  15240  lgsquad3  15241  2lgslem1a1  15243  2lgslem1a  15245  2lgslem1c  15247  2sqlem2  15272  mul2sq  15273  2sqlem7  15278  bj-inex  15469  bj-bdfindis  15509  triap  15589  cvgcmp2nlemabs  15592  trilpolemisumle  15598  inffz  15632