Theorem syl2an 287

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  syl2anr  288  anim12i  336  syl2an2  584  syl2an2r  585  mp3an3an  1333  eqeqan12d  2181  sylan9eq  2219  csbcomg  3068  sylan9ss  3155  ssconb  3255  ineqan12d  3325  dfopg  3756  breqan12d  3998  opexg  4206  copsex2g  4224  ordin  4363  onin  4364  unexg  4421  eusv1  4430  opelvvg  4653  opthprc  4655  opbrop  4683  relop  4754  dmpropg  5076  unixpm  5139  funssres  5230  funinsn  5237  funtp  5241  fnco  5296  resasplitss  5367  fodmrnu  5418  relrnfvex  5504  fconst2g  5700  oveqan12d  5861  ovi3  5978  ovg  5980  f1opw2  6044  off  6062  offres  6103  iunon  6252  nnsucsssuc  6460  nnaword1  6481  ertr  6516  erex  6525  brecop  6591  ecovdi  6612  ecovidi  6613  mapvalg  6624  pmvalg  6625  pmss12g  6641  mapsn  6656  en2sn  6779  xpf1o  6810  xpen  6811  phplem4  6821  ssfilem  6841  diffitest  6853  en1eqsn  6913  sbthlem7  6928  ordiso  7001  updjud  7047  fodju0  7111  finnum  7139  pr2nelem  7147  djucomen  7172  exmidontriimlem1  7177  ltsopi  7261  pitric  7262  pitri3or  7263  ltdcpi  7264  mulclpi  7269  addcompig  7270  mulcompig  7272  distrpig  7274  ltexpi  7278  ltapig  7279  ltmpig  7280  dfplpq2  7295  dfmpq2  7296  enqbreq2  7298  enqdc  7302  addcmpblnq  7308  addpipqqslem  7310  mulpipq2  7312  mulpipq  7313  mulpipqqs  7314  addclnq  7316  distrnqg  7328  ltdcnq  7338  ltrnqg  7361  enq0breq  7377  addclnq0  7392  nqnq0a  7395  nqnq0m  7396  nq0m0r  7397  distrnq0  7400  mulcomnq0  7401  genipv  7450  genplt2i  7451  genpelvl  7453  genpelvu  7454  addnqprlemrl  7498  addnqprlemru  7499  addnqprlemfl  7500  addnqprlemfu  7501  addnqpr  7502  mulnqprlemrl  7514  mulnqprlemru  7515  mulnqprlemfl  7516  mulnqprlemfu  7517  mulnqpr  7518  distrlem4prl  7525  distrlem4pru  7526  ltnqpr  7534  recexprlemloc  7572  archrecnq  7604  mulclsr  7695  1idsr  7709  00sr  7710  prsradd  7727  axmulass  7814  axdistr  7815  axcnre  7822  peano5nnnn  7833  mulid1  7896  axltadd  7968  lenlt  7974  cnegexlem3  8075  cnegex  8076  resubcl  8162  subeqrev  8274  muladd  8282  mulsub  8299  mulsub2  8300  ltaddsub2  8335  leaddsub2  8337  leltadd  8345  ltaddpos2  8351  posdif  8353  addge02  8371  mullt0  8378  recexre  8476  recextlem1  8548  recexap  8550  divmuldivap  8608  conjmulap  8625  div2subap  8733  prodgt02  8748  prodge02  8750  lemul2  8752  lemul2a  8754  ltmulgt12  8760  lemulge12  8762  ltmuldiv2  8770  ltdivmul2  8773  ledivmul2  8775  lemuldiv2  8777  negiso  8850  cju  8856  peano5nni  8860  nnaddcl  8877  nnmulcl  8878  nnsub  8896  addltmul  9093  avgle1  9097  avgle2  9098  nnrecl  9112  nn0nnaddcl  9145  zsubcl  9232  zleloe  9238  znnsub  9242  nzadd  9243  zmulcl  9244  zltp1le  9245  zleltp1  9246  nnleltp1  9250  nnltp1le  9251  nnaddm1cl  9252  nn0ltp1le  9253  nn0leltp1  9254  nn0ltlem1  9255  znn0sub  9256  nn0sub  9257  elz2  9262  zapne  9265  zdcle  9267  zdclt  9268  zltlen  9269  nn0lem1lt  9274  nnlem1lt  9275  nnltlem1  9276  zdiv  9279  zextle  9282  zextlt  9283  btwnnz  9285  prime  9290  nneo  9294  peano2uz2  9298  peano5uzti  9299  uzind  9302  fzind  9306  fnn0ind  9307  uzneg  9484  uz11  9488  eluzp1m1  9489  eluzp1p1  9491  uzin  9498  indstr  9531  uz2mulcl  9546  qre  9563  qaddcl  9573  qsubcl  9576  qltlen  9578  qlttri2  9579  irradd  9584  elpqb  9587  cnref1o  9588  rpaddcl  9613  rpmulcl  9614  rpdivcl  9615  rexadd  9788  rexsub  9789  xaddcom  9797  xnn0xadd0  9803  xnegdi  9804  elicc2  9874  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  fzval2  9947  elfz1eq  9970  peano2fzr  9972  fznlem  9976  fzsplit2  9985  fzaddel  9994  fzsubel  9995  fzrev2  10020  fzrev3  10022  uzsplit  10027  fzrevral  10040  fzrevral3  10042  fzshftral  10043  elfz2nn0  10047  fznn0sub2  10063  fz0fzdiffz0  10065  elfzmlbp  10067  difelfzle  10069  difelfznle  10070  1fv  10074  elfzouz2  10096  fzouzsplit  10114  elfzo0le  10120  fzonmapblen  10122  fzofzim  10123  fzoaddel2  10128  eluzgtdifelfzo  10132  elfzodifsumelfzo  10136  ubmelm1fzo  10161  fzofzp1b  10163  fzosplitprm1  10169  fzostep1  10172  subfzo0  10177  qbtwnxr  10193  flqbi2  10226  divfl0  10231  flqzadd  10233  flqmulnn0  10234  addmodidr  10308  modfzo0difsn  10330  frec2uzltd  10338  frec2uzrand  10340  frecfzen2  10362  seq3split  10414  seq3caopr2  10417  exp3vallem  10456  expcllem  10466  expcl2lemap  10467  1exp  10484  expge1  10492  expadd  10497  expmul  10500  expsubap  10503  leexp1a  10510  lt2sq  10528  le2sq  10529  sumsqeq0  10533  qsqeqor  10565  bernneq  10575  bernneq2  10576  sq11ap  10622  facdiv  10651  faclbnd  10654  faclbnd3  10656  faclbnd6  10657  facavg  10659  bcrpcl  10666  bccmpl  10667  fiubm  10741  seq3coll  10755  shftfvalg  10760  shftf  10772  crre  10799  crim  10800  mulreap  10806  readd  10811  resub  10812  remul2  10815  imadd  10819  imsub  10820  immul2  10822  ipcnval  10828  cjsub  10834  cjreim  10845  caucvgre  10923  rexanuz  10930  rexuz3  10932  resqrexlemover  10952  resqrexlemcvg  10961  resqrexlemglsq  10964  sqrtle  10978  sqrtlt  10979  sqrt11ap  10980  sqrt11  10981  absreimsq  11009  absreim  11010  absmul  11011  sqabs  11024  absdiflt  11034  absdifle  11035  abssuble0  11045  abs2difabs  11050  fzomaxdif  11055  caubnd2  11059  rpmaxcl  11165  zmaxcl  11166  minmax  11171  mincl  11172  min1inf  11173  min2inf  11174  minabs  11177  minclpr  11178  rpmincl  11179  2zinfmin  11184  xrmaxrecl  11196  xrminmax  11206  xrmincl  11207  xrmin1inf  11208  xrmin2inf  11209  xrminrecl  11214  xrminrpcl  11215  iooinsup  11218  climconst2  11232  climuni  11234  2clim  11242  climshft  11245  climshft2  11247  cjcn2  11257  climaddc1  11270  climmulc2  11272  climsubc1  11273  climsubc2  11274  climlec2  11282  summodclem2a  11322  zsumdc  11325  isumclim3  11364  mptfzshft  11383  fsumrev  11384  fisum0diag2  11388  telfsumo2  11408  fsumparts  11411  cvgcmpub  11417  binomlem  11424  binom1p  11426  binom1dif  11428  bcxmas  11430  isumshft  11431  expcnvap0  11443  expcnv  11445  geosergap  11447  geolim  11452  cvgratnnlemrate  11471  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodmodc  11519  zproddc  11520  fprodf1o  11529  fprodeq0  11558  efcj  11614  eftlub  11631  effsumlt  11633  efieq  11676  sinsub  11681  cossub  11682  subsin  11684  sinmul  11685  cosmul  11686  addcos  11687  subcos  11688  dvdssub2  11775  dvdsadd  11776  dvdsaddr  11777  dvdssub  11778  dvdssubr  11779  fzocongeq  11796  odd2np1  11810  opoe  11832  omoe  11833  opeo  11834  omeo  11835  divalgb  11862  ndvdsadd  11868  zsupcllemstep  11878  gcdabs  11921  dvdsgcd  11945  absmulgcd  11950  gcdmultiple  11953  gcdmultiplez  11954  rpmulgcd  11959  sqgcd  11962  dvdssqlem  11963  dvdssq  11964  nn0seqcvgd  11973  ialgrlemconst  11975  algrf  11977  algrp1  11978  algcvg  11980  algcvga  11983  lcmval  11995  lcmabs  12008  lcmgcd  12010  lcmdvds  12011  lcmgcdnn  12014  coprmgcdb  12020  coprmdvds  12024  coprmdvds2  12025  qredeq  12028  isprm3  12050  nprm  12055  divgcdodd  12075  prmdvdsexp  12080  sqrt2irr  12094  zgcdsq  12133  hashdvds  12153  phiprmpw  12154  crth  12156  phimullem  12157  modprm0  12186  coprimeprodsq  12189  coprimeprodsq2  12190  pythagtriplem2  12198  pythagtriplem19  12214  pcdvdsb  12251  pcneg  12256  pc2dvds  12261  pc11  12262  pcmpt  12273  pcfac  12280  infpnlem1  12289  prmunb  12292  1arithlem4  12296  1arith  12297  gzaddcl  12307  gzmulcl  12308  gzreim  12309  gzsubcl  12310  4sqlem1  12318  4sqlem4a  12321  4sqlem4  12322  setsvalg  12424  setsfun0  12430  restval  12562  innei  12803  cnovex  12836  txuni2  12896  txbasex  12897  txbas  12898  txtop  12900  txtopon  12902  txss12  12906  txbasval  12907  txcnp  12911  upxp  12912  txcnmpt  12913  uptx  12914  txcn  12915  txrest  12916  txdis  12917  cnmpt21  12931  hmeoco  12956  txhmeo  12959  isxmet2d  12988  blin2  13072  comet  13139  metcn  13154  txmetcn  13159  qtopbasss  13161  qtopbas  13162  remetdval  13179  bl2ioo  13182  blssioo  13185  divcnap  13195  cncfmet  13219  dvaddxxbr  13305  dvcjbr  13312  efle  13337  reapef  13339  sinperlem  13369  sincosq2sgn  13388  sincosq3sgn  13389  sincos6thpi  13403  ioocosf1o  13415  relogoprlem  13429  logleb  13436  cxple3  13481  cxpcom  13497  lgslem3  13543  lgsdir2  13574  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  2sqlem2  13591  mul2sq  13592  2sqlem7  13597  bj-inex  13789  bj-bdfindis  13829  triap  13908  cvgcmp2nlemabs  13911  trilpolemisumle  13917  inffz  13948