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  942  mp3an3an  1356  eqeqan12d  2222  sylan9eq  2259  csbcomg  3117  sylan9ss  3207  ssconb  3307  ineqan12d  3377  dfopg  3819  breqan12d  4063  opexg  4276  copsex2g  4294  ordin  4436  onin  4437  unexg  4494  eusv1  4503  opelvvg  4728  opthprc  4730  opbrop  4758  relop  4832  dmpropg  5160  unixpm  5223  funssres  5318  funinsn  5328  funtp  5332  fnco  5389  resasplitss  5462  fodmrnu  5513  relrnfvex  5601  funopdmsn  5771  fconst2g  5806  oveqan12d  5970  ovi3  6090  ovg  6092  f1opw2  6159  off  6178  offres  6227  iunon  6377  nnsucsssuc  6585  nnaword1  6606  ertr  6642  erex  6651  brecop  6719  ecovdi  6740  ecovidi  6741  mapvalg  6752  pmvalg  6753  pmss12g  6769  mapsn  6784  en2sn  6912  xpf1o  6948  xpen  6949  phplem4  6959  ssfilem  6979  diffitest  6991  en1eqsn  7057  sbthlem7  7072  ordiso  7145  updjud  7191  fodju0  7256  finnum  7297  pr2nelem  7306  djucomen  7335  exmidontriimlem1  7340  2onetap  7374  ltsopi  7440  pitric  7441  pitri3or  7442  ltdcpi  7443  mulclpi  7448  addcompig  7449  mulcompig  7451  distrpig  7453  ltexpi  7457  ltapig  7458  ltmpig  7459  dfplpq2  7474  dfmpq2  7475  enqbreq2  7477  enqdc  7481  addcmpblnq  7487  addpipqqslem  7489  mulpipq2  7491  mulpipq  7492  mulpipqqs  7493  addclnq  7495  distrnqg  7507  ltdcnq  7517  ltrnqg  7540  enq0breq  7556  addclnq0  7571  nqnq0a  7574  nqnq0m  7575  nq0m0r  7576  distrnq0  7579  mulcomnq0  7580  genipv  7629  genplt2i  7630  genpelvl  7632  genpelvu  7633  addnqprlemrl  7677  addnqprlemru  7678  addnqprlemfl  7679  addnqprlemfu  7680  addnqpr  7681  mulnqprlemrl  7693  mulnqprlemru  7694  mulnqprlemfl  7695  mulnqprlemfu  7696  mulnqpr  7697  distrlem4prl  7704  distrlem4pru  7705  ltnqpr  7713  recexprlemloc  7751  archrecnq  7783  mulclsr  7874  1idsr  7888  00sr  7889  prsradd  7906  axmulass  7993  axdistr  7994  axcnre  8001  peano5nnnn  8012  mulrid  8076  axltadd  8149  lenlt  8155  cnegexlem3  8256  cnegex  8257  resubcl  8343  subeqrev  8455  muladd  8463  mulsub  8480  mulsub2  8481  ltaddsub2  8517  leaddsub2  8519  leltadd  8527  ltaddpos2  8533  posdif  8535  addge02  8553  mullt0  8560  recexre  8658  recextlem1  8731  recexap  8733  divmuldivap  8792  conjmulap  8809  div2subap  8917  prodgt02  8933  prodge02  8935  lemul2  8937  lemul2a  8939  ltmulgt12  8945  lemulge12  8947  ltmuldiv2  8955  ltdivmul2  8958  ledivmul2  8960  lemuldiv2  8962  negiso  9035  cju  9041  peano5nni  9046  nnaddcl  9063  nnmulcl  9064  nnsub  9082  addltmul  9281  avgle1  9285  avgle2  9286  nnrecl  9300  nn0nnaddcl  9333  zsubcl  9420  zleloe  9426  znnsub  9431  nzadd  9432  zmulcl  9433  zltp1le  9434  zleltp1  9435  nnleltp1  9439  nnltp1le  9440  nnaddm1cl  9441  nn0ltp1le  9442  nn0leltp1  9443  nn0ltlem1  9444  znn0sub  9445  nn0sub  9446  elz2  9451  zapne  9454  zdcle  9456  zdclt  9457  zltlen  9458  nn0lem1lt  9463  nnlem1lt  9464  nnltlem1  9465  zdiv  9468  zextle  9471  zextlt  9472  btwnnz  9474  prime  9479  nneo  9483  peano2uz2  9487  peano5uzti  9488  uzind  9491  fzind  9495  fnn0ind  9496  uzneg  9674  uz11  9678  eluzp1m1  9679  eluzp1p1  9681  uzin  9688  indstr  9721  uz2mulcl  9736  qre  9753  qaddcl  9763  qsubcl  9766  qltlen  9768  qlttri2  9769  irradd  9774  elpqb  9778  cnref1o  9779  rpaddcl  9806  rpmulcl  9807  rpdivcl  9808  rexadd  9981  rexsub  9982  xaddcom  9990  xnn0xadd0  9996  xnegdi  9997  elicc2  10067  iccshftr  10123  iccshftl  10125  iccdil  10127  icccntr  10129  fzval2  10140  elfz1eq  10164  peano2fzr  10166  fznlem  10170  fzsplit2  10179  fzaddel  10188  fzsubel  10189  fzrev2  10214  fzrev3  10216  uzsplit  10221  fzrevral  10234  fzrevral3  10236  fzshftral  10237  elfz2nn0  10241  fznn0sub2  10257  fz0fzdiffz0  10259  elfzmlbp  10261  difelfzle  10263  difelfznle  10264  1fv  10268  elfzouz2  10291  fzo0n  10297  fzouzsplit  10310  elfzo0le  10316  fzonmapblen  10318  fzofzim  10319  fzoaddel2  10326  eluzgtdifelfzo  10333  elfzodifsumelfzo  10337  ubmelm1fzo  10362  fzofzp1b  10364  fzosplitprm1  10370  fzostep1  10373  subfzo0  10378  zsupcllemstep  10379  qdclt  10395  qbtwnxr  10407  flqbi2  10441  divfl0  10446  flqzadd  10448  flqmulnn0  10449  addmodidr  10525  modfzo0difsn  10547  frec2uzltd  10555  frec2uzrand  10557  frecfzen2  10579  seqshft2g  10634  seq3split  10640  seqsplitg  10641  seq3caopr2  10645  seqcaopr2g  10646  seqf1oglem2  10672  exp3vallem  10692  expcllem  10702  expcl2lemap  10703  1exp  10720  expge1  10728  expadd  10733  expmul  10736  expsubap  10739  leexp1a  10746  lt2sq  10765  le2sq  10766  sumsqeq0  10770  qsqeqor  10802  bernneq  10812  bernneq2  10813  sq11ap  10859  facdiv  10890  faclbnd  10893  faclbnd3  10895  faclbnd6  10896  facavg  10898  bcrpcl  10905  bccmpl  10906  fiubm  10980  seq3coll  10994  eqwrd  11041  ccatcl  11057  ccatclab  11058  ccatlen  11059  ccat0  11060  ccatval1  11061  ccatval2  11062  elfzelfzccat  11064  ccatvalfn  11065  ccatsymb  11066  ccatval21sw  11069  ccatrn  11073  lswccatn0lsw  11075  swrdfv2  11124  swrdsbslen  11127  swrdspsleq  11128  swrdccat2  11132  ccatpfx  11160  pfxccat1  11161  swrdswrdlem  11163  pfxswrd  11165  shftfvalg  11173  shftf  11185  crre  11212  crim  11213  mulreap  11219  readd  11224  resub  11225  remul2  11228  imadd  11232  imsub  11233  immul2  11235  ipcnval  11241  cjsub  11247  cjreim  11258  caucvgre  11336  rexanuz  11343  rexuz3  11345  resqrexlemover  11365  resqrexlemcvg  11374  resqrexlemglsq  11377  sqrtle  11391  sqrtlt  11392  sqrt11ap  11393  sqrt11  11394  absreimsq  11422  absreim  11423  absmul  11424  sqabs  11437  absdiflt  11447  absdifle  11448  abssuble0  11458  abs2difabs  11463  fzomaxdif  11468  caubnd2  11472  rpmaxcl  11578  zmaxcl  11579  nn0maxcl  11580  minmax  11585  mincl  11586  min1inf  11587  min2inf  11588  minabs  11591  minclpr  11592  rpmincl  11593  2zinfmin  11598  xrmaxrecl  11610  xrminmax  11620  xrmincl  11621  xrmin1inf  11622  xrmin2inf  11623  xrminrecl  11628  xrminrpcl  11629  iooinsup  11632  climconst2  11646  climuni  11648  2clim  11656  climshft  11659  climshft2  11661  cjcn2  11671  climaddc1  11684  climmulc2  11686  climsubc1  11687  climsubc2  11688  climlec2  11696  summodclem2a  11736  zsumdc  11739  isumclim3  11778  mptfzshft  11797  fsumrev  11798  fisum0diag2  11802  telfsumo2  11822  fsumparts  11825  cvgcmpub  11831  binomlem  11838  binom1p  11840  binom1dif  11842  bcxmas  11844  isumshft  11845  expcnvap0  11857  expcnv  11859  geosergap  11861  geolim  11866  cvgratnnlemrate  11885  mertenslemi1  11890  mertenslem2  11891  mertensabs  11892  prodmodc  11933  zproddc  11934  fprodf1o  11943  fprodeq0  11972  efcj  12028  eftlub  12045  effsumlt  12047  efieq  12090  sinsub  12095  cossub  12096  subsin  12098  sinmul  12099  cosmul  12100  addcos  12101  subcos  12102  dvdssub2  12190  dvdsadd  12191  dvdsaddr  12192  dvdssub  12193  dvdssubr  12194  fzocongeq  12213  odd2np1  12228  opoe  12250  omoe  12251  opeo  12252  omeo  12253  divalgb  12280  ndvdsadd  12286  bitsfi  12312  gcdmndc  12320  gcdabs  12353  dvdsgcd  12377  absmulgcd  12382  gcdmultiple  12385  gcdmultiplez  12386  rpmulgcd  12391  sqgcd  12394  dvdssqlem  12395  dvdssq  12396  nninfctlemfo  12405  nn0seqcvgd  12407  ialgrlemconst  12409  algrf  12411  algrp1  12412  algcvg  12414  algcvga  12417  lcmval  12429  lcmabs  12442  lcmgcd  12444  lcmdvds  12445  lcmgcdnn  12448  coprmgcdb  12454  coprmdvds  12458  coprmdvds2  12459  qredeq  12462  isprm3  12484  nprm  12489  divgcdodd  12509  prmdvdsexp  12514  sqrt2irr  12528  zgcdsq  12567  hashdvds  12587  phiprmpw  12588  crth  12590  phimullem  12591  modprm0  12621  coprimeprodsq  12624  coprimeprodsq2  12625  pythagtriplem2  12633  pythagtriplem19  12649  pcdvdsb  12687  pcneg  12692  pc2dvds  12697  pc11  12698  pcmpt  12710  pcfac  12717  infpnlem1  12726  prmunb  12729  1arithlem4  12733  1arith  12734  gzaddcl  12744  gzmulcl  12745  gzreim  12746  gzsubcl  12747  4sqlem1  12755  4sqlem4a  12758  4sqlem4  12759  4sqlem12  12769  setsvalg  12906  setsfun0  12912  restval  13121  xpsval  13228  mndinvmod  13321  resmhm  13363  resmhm2  13364  mhmco  13366  dfgrp3m  13475  mhmmnd  13496  mulgnngsum  13507  mulgnn0z  13529  mulgnndir  13531  ghmex  13635  0ghm  13638  resghm  13640  resghm2  13641  ghmco  13644  ghmeql  13647  kerf1ghm  13654  ablsubsub23  13705  dfrhm2  13960  isrhm  13964  rhmfn  13978  rhmval  13979  rhmco  13980  resrhm  14054  rhmeql  14056  rhmima  14057  lmodfopne  14132  lspf  14195  znidom  14463  znrrg  14466  innei  14679  cnovex  14712  txuni2  14772  txbasex  14773  txbas  14774  txtop  14776  txtopon  14778  txss12  14782  txbasval  14783  txcnp  14787  upxp  14788  txcnmpt  14789  uptx  14790  txcn  14791  txrest  14792  txdis  14793  cnmpt21  14807  hmeoco  14832  txhmeo  14835  isxmet2d  14864  blin2  14948  comet  15015  metcn  15030  txmetcn  15035  qtopbasss  15037  qtopbas  15038  remetdval  15063  bl2ioo  15066  blssioo  15069  divcnap  15081  cncfmet  15108  dvaddxxbr  15217  dvcjbr  15224  plyf  15253  ply1termlem  15258  plymullem1  15264  plyaddlem  15265  plymullem  15266  plycolemc  15274  plyreres  15280  dvply1  15281  efle  15292  reapef  15294  sinperlem  15324  sincosq2sgn  15343  sincosq3sgn  15344  sincos6thpi  15358  ioocosf1o  15370  relogoprlem  15384  logleb  15391  cxple3  15437  cxpcom  15454  dvdsppwf1o  15505  fsumdvdsmul  15507  1sgmprm  15510  mersenne  15513  lgslem3  15523  lgsdir2  15554  lgsdir  15556  lgsdilem2  15557  lgsdi  15558  gausslemma2dlem1a  15579  gausslemma2dlem3  15584  gausslemma2dlem6  15588  lgseisenlem3  15593  lgseisenlem4  15594  lgsquadlem1  15598  lgsquadlem2  15599  lgsquad2  15604  lgsquad3  15605  2lgslem1a1  15607  2lgslem1a  15609  2lgslem1c  15611  2sqlem2  15636  mul2sq  15637  2sqlem7  15642  bj-inex  15917  bj-bdfindis  15957  triap  16042  cvgcmp2nlemabs  16045  trilpolemisumle  16051  inffz  16085