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 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  syl2anr  290  anim12i  338  syl2an2  602  syl2an2r  603  orandc  952  mp3an3an  1384  eqeqan12d  2254  sylan9eq  2291  csbcomg  3170  sylan9ss  3261  ssconb  3362  ineqan12d  3434  dfopg  3902  breqan12d  4146  opexg  4368  copsex2g  4386  ordin  4530  onin  4531  unexg  4589  eusv1  4598  opelvvg  4824  opthprc  4826  opbrop  4854  relop  4930  dmpropg  5260  unixpm  5323  funssres  5420  funinsn  5430  funtp  5434  fnco  5491  resasplitss  5569  fodmrnu  5623  relrnfvex  5713  funopdmsn  5895  fconst2g  5930  oveqan12d  6104  ovi3  6226  ovg  6228  f1opw2  6296  off  6315  offres  6368  suppfnss  6497  iunon  6555  nnsucsssuc  6765  nnaword1  6786  ertr  6822  erex  6831  brecop  6899  ecovdi  6920  ecovidi  6921  mapvalg  6932  pmvalg  6933  pmss12g  6956  mapsn  6972  en2sn  7102  xpf1o  7144  xpen  7145  phplem4  7156  ssfilem  7177  ssfilemd  7179  diffitest  7191  en1eqsn  7265  sbthlem7  7280  fsuppxpfi  7296  ordiso  7377  updjud  7423  fodju0  7488  finnum  7529  pr2nelem  7538  djucomen  7573  exmidontriimlem1  7578  2onetap  7622  ltsopi  7688  pitric  7689  pitri3or  7690  ltdcpi  7691  mulclpi  7696  addcompig  7697  mulcompig  7699  distrpig  7701  ltexpi  7705  ltapig  7706  ltmpig  7707  dfplpq2  7722  dfmpq2  7723  enqbreq2  7725  enqdc  7729  addcmpblnq  7735  addpipqqslem  7737  mulpipq2  7739  mulpipq  7740  mulpipqqs  7741  addclnq  7743  distrnqg  7755  ltdcnq  7765  ltrnqg  7788  enq0breq  7804  addclnq0  7819  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  distrnq0  7827  mulcomnq0  7828  genipv  7877  genplt2i  7878  genpelvl  7880  genpelvu  7881  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  addnqpr  7929  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  mulnqpr  7945  distrlem4prl  7952  distrlem4pru  7953  ltnqpr  7961  recexprlemloc  7999  archrecnq  8031  mulclsr  8122  1idsr  8136  00sr  8137  prsradd  8154  axmulass  8241  axdistr  8242  axcnre  8249  peano5nnnn  8260  mulrid  8324  axltadd  8396  lenlt  8402  cnegexlem3  8505  cnegex  8506  resubcl  8592  subeqrev  8704  muladd  8713  mulsub  8730  mulsub2  8731  ltaddsub2  8767  leaddsub2  8769  leltadd  8777  ltaddpos2  8783  posdif  8785  addge02  8803  mullt0  8810  recexre  8909  recextlem1  8982  recexap  8984  divmuldivap  9045  conjmulap  9062  div2subap  9170  prodgt02  9186  prodge02  9188  lemul2  9190  lemul2a  9192  ltmulgt12  9198  lemulge12  9200  ltmuldiv2  9208  ltdivmul2  9211  ledivmul2  9213  lemuldiv2  9215  negiso  9288  cju  9294  peano5nni  9310  nnaddcl  9327  nnmulcl  9328  nnsub  9346  addltmul  9547  avgle1  9551  avgle2  9552  nnrecl  9566  nn0nnaddcl  9599  zsubcl  9690  zleloe  9696  znnsub  9701  nzadd  9702  zmulcl  9703  zltp1le  9704  zleltp1  9705  nnleltp1  9709  nnltp1le  9710  nnaddm1cl  9711  nn0ltp1le  9712  nn0leltp1  9713  nn0ltlem1  9714  znn0sub  9715  nn0sub  9716  elz2  9721  zapne  9724  zdcle  9726  zdclt  9727  zltlen  9729  nn0lem1lt  9734  nnlem1lt  9735  nnltlem1  9736  zdiv  9739  zextle  9742  zextlt  9743  btwnnz  9745  prime  9750  nneo  9754  peano2uz2  9758  peano5uzti  9759  uzind  9762  fzind  9766  fnn0ind  9767  uzneg  9951  uz11  9955  eluzp1m1  9956  eluzp1p1  9958  uzin  9965  indstr  10003  uz2mulcl  10018  qre  10035  qaddcl  10045  qsubcl  10048  qltlen  10050  qlttri2  10051  irradd  10056  elpqb  10061  cnref1o  10062  rpaddcl  10089  rpmulcl  10090  rpdivcl  10091  rexadd  10265  rexsub  10266  xaddcom  10274  xnn0xadd0  10280  xnegdi  10281  elicc2  10351  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzval2  10425  elfz1eq  10450  peano2fzr  10452  fznlem  10456  fzsplit2  10466  fzsplit3  10469  fzaddel  10476  fzsubel  10477  fzrev2  10503  fzrev3  10505  uzsplit  10510  fzrevral  10523  fzrevral3  10525  fzshftral  10526  elfz2nn0  10530  fznn0sub2  10546  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  difelfznle  10553  1fv  10557  elfzouz2  10580  fzo0n  10586  fzouzsplit  10599  fzoun  10601  elfzo0le  10608  fzonmapblen  10610  fzofzim  10611  fzoaddel2  10619  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  ubmelm1fzo  10655  fzofzp1b  10657  fzosplitprm1  10664  fzostep1  10667  subfzo0  10672  zsupcllemstep  10673  qdclt  10691  qbtwnxr  10703  flqbi2  10741  divfl0  10746  flqzadd  10748  flqmulnn0  10749  addmodidr  10825  modfzo0difsn  10847  frec2uzltd  10855  frec2uzrand  10857  frecfzen2  10879  seqshft2g  10934  seq3split  10940  seqsplitg  10941  seq3caopr2  10945  seqcaopr2g  10946  seqf1oglem2  10972  exp3vallem  10992  expcllem  11002  expcl2lemap  11003  1exp  11020  expge1  11028  expadd  11033  expmul  11036  expsubap  11039  leexp1a  11046  lt2sq  11065  le2sq  11066  sumsqeq0  11070  qsqeqor  11102  bernneq  11113  bernneq2  11114  sq11ap  11160  facdiv  11192  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  facavg  11200  bcrpcl  11207  bccmpl  11208  bcm1n  11223  fiubm  11287  seq3coll  11310  eqwrd  11361  ccatcl  11377  ccatclab  11378  ccatlen  11379  ccat0  11380  ccatval1  11381  ccatval2  11382  elfzelfzccat  11384  ccatvalfn  11385  ccatsymb  11386  ccatval21sw  11389  ccatrn  11393  lswccatn0lsw  11395  ccatalpha  11397  ccatrcl1  11398  swrdfv2  11451  swrdsbslen  11454  swrdspsleq  11455  swrdccat2  11459  pfxclz  11467  ccatpfx  11489  pfxccat1  11490  swrdswrdlem  11492  pfxswrd  11494  pfxccatin12lem4  11514  pfxccatin12lem1  11516  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccat3  11522  swrdccat  11523  pfxccatpfx2  11525  pfxccat3a  11526  swrdccat3blem  11527  swrdccat3b  11528  s2dmg  11578  shftfvalg  11599  shftf  11611  crre  11638  crim  11639  mulreap  11645  readd  11650  resub  11651  remul2  11654  imadd  11658  imsub  11659  immul2  11661  ipcnval  11667  cjsub  11673  cjreim  11685  caucvgre  11763  rexanuz  11770  rexuz3  11772  resqrexlemover  11792  resqrexlemcvg  11801  resqrexlemglsq  11804  sqrtle  11818  sqrtlt  11819  sqrt11ap  11820  sqrt11  11821  absreimsq  11849  absreim  11850  absmul  11851  sqabs  11865  absdiflt  11875  absdifle  11876  abssuble0  11886  abs2difabs  11891  fzomaxdif  11896  caubnd2  11900  rpmaxcl  12006  zmaxcl  12007  nn0maxcl  12008  minmax  12014  mincl  12015  min1inf  12016  min2inf  12017  minabs  12020  minclpr  12021  rpmincl  12022  zmincl  12023  2zinfmin  12028  xrmaxrecl  12040  xrminmax  12050  xrmincl  12051  xrmin1inf  12052  xrmin2inf  12053  xrminrecl  12058  xrminrpcl  12059  iooinsup  12062  climconst2  12076  climuni  12078  2clim  12086  climshft  12089  climshft2  12091  cjcn2  12101  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climlec2  12126  summodclem2a  12167  zsumdc  12170  isumclim3  12209  mptfzshft  12228  fsumrev  12229  fisum0diag2  12233  telfsumo2  12253  fsumparts  12256  cvgcmpub  12262  binomlem  12269  binom1p  12271  binom1dif  12273  bcxmas  12275  isumshft  12276  expcnvap0  12288  expcnv  12290  geosergap  12292  geolim  12297  cvgratnnlemrate  12316  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodmodc  12364  zproddc  12365  fprodf1o  12374  fprodeq0  12403  efcj  12459  eftlub  12476  effsumlt  12478  efieq  12521  sinsub  12526  cossub  12527  subsin  12529  sinmul  12530  cosmul  12531  addcos  12532  subcos  12533  dvdssub2  12621  dvdsadd  12622  dvdsaddr  12623  dvdssub  12624  dvdssubr  12625  fzocongeq  12644  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  divalgb  12711  ndvdsadd  12717  bitsfi  12743  gcdmndc  12751  gcdabs  12784  dvdsgcd  12808  absmulgcd  12813  gcdmultiple  12816  gcdmultiplez  12817  rpmulgcd  12822  sqgcd  12825  dvdssqlem  12826  dvdssq  12827  nninfctlemfo  12836  nn0seqcvgd  12838  ialgrlemconst  12840  algrf  12842  algrp1  12843  algcvg  12845  algcvga  12848  lcmval  12860  lcmabs  12873  lcmgcd  12875  lcmdvds  12876  lcmgcdnn  12879  coprmgcdb  12885  coprmdvds  12889  coprmdvds2  12890  qredeq  12893  isprm3  12915  nprm  12920  divgcdodd  12941  prmdvdsexp  12946  sqrt2irr  12960  zgcdsq  13000  hashdvds  13022  phiprmpw  13023  crth  13025  phimullem  13026  modprm0  13056  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem2  13068  pythagtriplem19  13084  pcdvdsb  13122  pcneg  13127  pc2dvds  13132  pc11  13133  pcmpt  13145  pcfac  13152  infpnlem1  13161  prmunb  13164  1arithlem4  13168  1arith  13169  gzaddcl  13179  gzmulcl  13180  gzreim  13181  gzsubcl  13182  4sqlem1  13190  4sqlem4a  13193  4sqlem4  13194  4sqlem12  13204  ballotfilemfc0  13284  ballotfilemfcc  13285  setsvalg  13434  setsfun0  13440  restval  13652  mndinvmod  13811  resmhm  13847  resmhm2  13848  mhmco  13850  dfgrp3m  13957  mhmmnd  13972  mulgnngzsum  13983  mulgnn0z  14005  mulgnndir  14007  ghmex  14111  0ghm  14114  resghm  14116  resghm2  14117  ghmco  14120  ghmeql  14123  kerf1ghm  14130  cntzmhm  14167  ablsubsub23  14213  xpsval  14285  dfrhm2  14545  isrhm  14549  rhmfn  14563  rhmval  14564  rhmco  14565  resrhm  14640  rhmeql  14642  rhmima  14643  lmodfopne  14747  lspf  14810  znidom  15076  znrrg  15079  issubassa3  15096  innei  15355  cnovex  15388  txuni2  15448  txbasex  15449  txbas  15450  txtop  15452  txtopon  15454  txss12  15458  txbasval  15459  txcnp  15463  upxp  15464  txcnmpt  15465  uptx  15466  txcn  15467  txrest  15468  txdis  15469  cnmpt21  15483  hmeoco  15508  txhmeo  15511  isxmet2d  15540  blin2  15624  comet  15691  metcn  15706  txmetcn  15711  qtopbasss  15713  qtopbas  15714  remetdval  15739  bl2ioo  15742  blssioo  15745  divcnap  15757  cncfmet  15784  dvaddxxbr  15893  dvcjbr  15900  plyf  15929  ply1termlem  15934  plymullem1  15940  plyaddlem  15941  plymullem  15942  plycolemc  15950  plyreres  15956  dvply1  15957  efle  15968  reapef  15970  sinperlem  16001  sincosq2sgn  16020  sincosq3sgn  16021  sincos6thpi  16035  ioocosf1o  16048  reaplog  16063  relogoprlem  16064  logleb  16071  cxple3  16122  cxpcom  16139  efnthr  16142  birthdaylem2  16192  birthdaylem3  16193  dvdsppwf1o  16249  fsumdvdsmul  16251  1sgmprm  16254  chtublem  16261  mersenne  16263  pcbcctr  16269  bcmono  16270  bposlem1  16277  bposlem2  16278  bposlem3  16279  bposlem5  16281  bposlem6  16282  bposlem7  16283  lgslem3  16292  lgsdir2  16323  lgsdir  16325  lgsdilem2  16326  lgsdi  16327  gausslemma2dlem1a  16348  gausslemma2dlem3  16353  gausslemma2dlem6  16357  lgseisenlem3  16362  lgseisenlem4  16363  lgsquadlem1  16367  lgsquadlem2  16368  lgsquad2  16373  lgsquad3  16374  2lgslem1a1  16376  2lgslem1a  16378  2lgslem1c  16380  2sqlem2  16405  mul2sq  16406  2sqlem7  16411  usgredg2v  16636  ushgredgedg  16638  ushgredgedgloop  16640  uhgrissubgr  16673  vtxedgfi  16701  vtxlpfi  16702  wlkeq  16766  uspgr2wlkeq  16777  clwwlkccatlem  16812  clwwlkccat  16813  clwwlknccat  16835  bj-inex  17104  bj-bdfindis  17144  triap  17249  cvgcmp2nlemabs  17252  trilpolemisumle  17259  inffz  17294