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  7376  updjud  7422  fodju0  7487  finnum  7528  pr2nelem  7537  djucomen  7572  exmidontriimlem1  7577  2onetap  7621  ltsopi  7687  pitric  7688  pitri3or  7689  ltdcpi  7690  mulclpi  7695  addcompig  7696  mulcompig  7698  distrpig  7700  ltexpi  7704  ltapig  7705  ltmpig  7706  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enqdc  7728  addcmpblnq  7734  addpipqqslem  7736  mulpipq2  7738  mulpipq  7739  mulpipqqs  7740  addclnq  7742  distrnqg  7754  ltdcnq  7764  ltrnqg  7787  enq0breq  7803  addclnq0  7818  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  distrnq0  7826  mulcomnq0  7827  genipv  7876  genplt2i  7877  genpelvl  7879  genpelvu  7880  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  addnqpr  7928  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  mulnqpr  7944  distrlem4prl  7951  distrlem4pru  7952  ltnqpr  7960  recexprlemloc  7998  archrecnq  8030  mulclsr  8121  1idsr  8135  00sr  8136  prsradd  8153  axmulass  8240  axdistr  8241  axcnre  8248  peano5nnnn  8259  mulrid  8323  axltadd  8395  lenlt  8401  cnegexlem3  8504  cnegex  8505  resubcl  8591  subeqrev  8703  muladd  8712  mulsub  8729  mulsub2  8730  ltaddsub2  8766  leaddsub2  8768  leltadd  8776  ltaddpos2  8782  posdif  8784  addge02  8802  mullt0  8809  recexre  8908  recextlem1  8981  recexap  8983  divmuldivap  9044  conjmulap  9061  div2subap  9169  prodgt02  9185  prodge02  9187  lemul2  9189  lemul2a  9191  ltmulgt12  9197  lemulge12  9199  ltmuldiv2  9207  ltdivmul2  9210  ledivmul2  9212  lemuldiv2  9214  negiso  9287  cju  9293  peano5nni  9309  nnaddcl  9326  nnmulcl  9327  nnsub  9345  addltmul  9546  avgle1  9550  avgle2  9551  nnrecl  9565  nn0nnaddcl  9598  zsubcl  9689  zleloe  9695  znnsub  9700  nzadd  9701  zmulcl  9702  zltp1le  9703  zleltp1  9704  nnleltp1  9708  nnltp1le  9709  nnaddm1cl  9710  nn0ltp1le  9711  nn0leltp1  9712  nn0ltlem1  9713  znn0sub  9714  nn0sub  9715  elz2  9720  zapne  9723  zdcle  9725  zdclt  9726  zltlen  9728  nn0lem1lt  9733  nnlem1lt  9734  nnltlem1  9735  zdiv  9738  zextle  9741  zextlt  9742  btwnnz  9744  prime  9749  nneo  9753  peano2uz2  9757  peano5uzti  9758  uzind  9761  fzind  9765  fnn0ind  9766  uzneg  9950  uz11  9954  eluzp1m1  9955  eluzp1p1  9957  uzin  9964  indstr  10002  uz2mulcl  10017  qre  10034  qaddcl  10044  qsubcl  10047  qltlen  10049  qlttri2  10050  irradd  10055  elpqb  10060  cnref1o  10061  rpaddcl  10088  rpmulcl  10089  rpdivcl  10090  rexadd  10264  rexsub  10265  xaddcom  10273  xnn0xadd0  10279  xnegdi  10280  elicc2  10350  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  fzval2  10424  elfz1eq  10449  peano2fzr  10451  fznlem  10455  fzsplit2  10465  fzsplit3  10468  fzaddel  10475  fzsubel  10476  fzrev2  10502  fzrev3  10504  uzsplit  10509  fzrevral  10522  fzrevral3  10524  fzshftral  10525  elfz2nn0  10529  fznn0sub2  10545  fz0fzdiffz0  10547  elfzmlbp  10549  difelfzle  10551  difelfznle  10552  1fv  10556  elfzouz2  10579  fzo0n  10585  fzouzsplit  10598  fzoun  10600  elfzo0le  10607  fzonmapblen  10609  fzofzim  10610  fzoaddel2  10618  eluzgtdifelfzo  10625  elfzodifsumelfzo  10629  ubmelm1fzo  10654  fzofzp1b  10656  fzosplitprm1  10663  fzostep1  10666  subfzo0  10671  zsupcllemstep  10672  qdclt  10690  qbtwnxr  10702  flqbi2  10739  divfl0  10744  flqzadd  10746  flqmulnn0  10747  addmodidr  10823  modfzo0difsn  10845  frec2uzltd  10853  frec2uzrand  10855  frecfzen2  10877  seqshft2g  10932  seq3split  10938  seqsplitg  10939  seq3caopr2  10943  seqcaopr2g  10944  seqf1oglem2  10970  exp3vallem  10990  expcllem  11000  expcl2lemap  11001  1exp  11018  expge1  11026  expadd  11031  expmul  11034  expsubap  11037  leexp1a  11044  lt2sq  11063  le2sq  11064  sumsqeq0  11068  qsqeqor  11100  bernneq  11111  bernneq2  11112  sq11ap  11158  facdiv  11190  faclbnd  11193  faclbnd3  11195  faclbnd6  11196  facavg  11198  bcrpcl  11205  bccmpl  11206  bcm1n  11221  fiubm  11285  seq3coll  11308  eqwrd  11359  ccatcl  11375  ccatclab  11376  ccatlen  11377  ccat0  11378  ccatval1  11379  ccatval2  11380  elfzelfzccat  11382  ccatvalfn  11383  ccatsymb  11384  ccatval21sw  11387  ccatrn  11391  lswccatn0lsw  11393  ccatalpha  11395  ccatrcl1  11396  swrdfv2  11449  swrdsbslen  11452  swrdspsleq  11453  swrdccat2  11457  pfxclz  11465  ccatpfx  11487  pfxccat1  11488  swrdswrdlem  11490  pfxswrd  11492  pfxccatin12lem4  11512  pfxccatin12lem1  11514  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccat3  11520  swrdccat  11521  pfxccatpfx2  11523  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  s2dmg  11576  shftfvalg  11597  shftf  11609  crre  11636  crim  11637  mulreap  11643  readd  11648  resub  11649  remul2  11652  imadd  11656  imsub  11657  immul2  11659  ipcnval  11665  cjsub  11671  cjreim  11683  caucvgre  11761  rexanuz  11768  rexuz3  11770  resqrexlemover  11790  resqrexlemcvg  11799  resqrexlemglsq  11802  sqrtle  11816  sqrtlt  11817  sqrt11ap  11818  sqrt11  11819  absreimsq  11847  absreim  11848  absmul  11849  sqabs  11863  absdiflt  11873  absdifle  11874  abssuble0  11884  abs2difabs  11889  fzomaxdif  11894  caubnd2  11898  rpmaxcl  12004  zmaxcl  12005  nn0maxcl  12006  minmax  12011  mincl  12012  min1inf  12013  min2inf  12014  minabs  12017  minclpr  12018  rpmincl  12019  zmincl  12020  2zinfmin  12025  xrmaxrecl  12037  xrminmax  12047  xrmincl  12048  xrmin1inf  12049  xrmin2inf  12050  xrminrecl  12055  xrminrpcl  12056  iooinsup  12059  climconst2  12073  climuni  12075  2clim  12083  climshft  12086  climshft2  12088  cjcn2  12098  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  climlec2  12123  summodclem2a  12164  zsumdc  12167  isumclim3  12206  mptfzshft  12225  fsumrev  12226  fisum0diag2  12230  telfsumo2  12250  fsumparts  12253  cvgcmpub  12259  binomlem  12266  binom1p  12268  binom1dif  12270  bcxmas  12272  isumshft  12273  expcnvap0  12285  expcnv  12287  geosergap  12289  geolim  12294  cvgratnnlemrate  12313  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodmodc  12361  zproddc  12362  fprodf1o  12371  fprodeq0  12400  efcj  12456  eftlub  12473  effsumlt  12475  efieq  12518  sinsub  12523  cossub  12524  subsin  12526  sinmul  12527  cosmul  12528  addcos  12529  subcos  12530  dvdssub2  12618  dvdsadd  12619  dvdsaddr  12620  dvdssub  12621  dvdssubr  12622  fzocongeq  12641  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  divalgb  12708  ndvdsadd  12714  bitsfi  12740  gcdmndc  12748  gcdabs  12781  dvdsgcd  12805  absmulgcd  12810  gcdmultiple  12813  gcdmultiplez  12814  rpmulgcd  12819  sqgcd  12822  dvdssqlem  12823  dvdssq  12824  nninfctlemfo  12833  nn0seqcvgd  12835  ialgrlemconst  12837  algrf  12839  algrp1  12840  algcvg  12842  algcvga  12845  lcmval  12857  lcmabs  12870  lcmgcd  12872  lcmdvds  12873  lcmgcdnn  12876  coprmgcdb  12882  coprmdvds  12886  coprmdvds2  12887  qredeq  12890  isprm3  12912  nprm  12917  divgcdodd  12938  prmdvdsexp  12943  sqrt2irr  12957  zgcdsq  12997  hashdvds  13019  phiprmpw  13020  crth  13022  phimullem  13023  modprm0  13053  coprimeprodsq  13056  coprimeprodsq2  13057  pythagtriplem2  13065  pythagtriplem19  13081  pcdvdsb  13119  pcneg  13124  pc2dvds  13129  pc11  13130  pcmpt  13142  pcfac  13149  infpnlem1  13158  prmunb  13161  1arithlem4  13165  1arith  13166  gzaddcl  13176  gzmulcl  13177  gzreim  13178  gzsubcl  13179  4sqlem1  13187  4sqlem4a  13190  4sqlem4  13191  4sqlem12  13201  ballotfilemfc0  13281  ballotfilemfcc  13282  setsvalg  13431  setsfun0  13437  restval  13648  mndinvmod  13807  resmhm  13843  resmhm2  13844  mhmco  13846  dfgrp3m  13953  mhmmnd  13968  mulgnngzsum  13979  mulgnn0z  14001  mulgnndir  14003  ghmex  14107  0ghm  14110  resghm  14112  resghm2  14113  ghmco  14116  ghmeql  14119  kerf1ghm  14126  ablsubsub23  14178  xpsval  14250  dfrhm2  14510  isrhm  14514  rhmfn  14528  rhmval  14529  rhmco  14530  resrhm  14605  rhmeql  14607  rhmima  14608  lmodfopne  14712  lspf  14775  znidom  15041  znrrg  15044  issubassa3  15061  innei  15313  cnovex  15346  txuni2  15406  txbasex  15407  txbas  15408  txtop  15410  txtopon  15412  txss12  15416  txbasval  15417  txcnp  15421  upxp  15422  txcnmpt  15423  uptx  15424  txcn  15425  txrest  15426  txdis  15427  cnmpt21  15441  hmeoco  15466  txhmeo  15469  isxmet2d  15498  blin2  15582  comet  15649  metcn  15664  txmetcn  15669  qtopbasss  15671  qtopbas  15672  remetdval  15697  bl2ioo  15700  blssioo  15703  divcnap  15715  cncfmet  15742  dvaddxxbr  15851  dvcjbr  15858  plyf  15887  ply1termlem  15892  plymullem1  15898  plyaddlem  15899  plymullem  15900  plycolemc  15908  plyreres  15914  dvply1  15915  efle  15926  reapef  15928  sinperlem  15959  sincosq2sgn  15978  sincosq3sgn  15979  sincos6thpi  15993  ioocosf1o  16005  reaplog  16019  relogoprlem  16020  logleb  16027  cxple3  16076  cxpcom  16093  birthdaylem2  16145  birthdaylem3  16146  dvdsppwf1o  16202  fsumdvdsmul  16204  1sgmprm  16207  chtublem  16214  mersenne  16216  pcbcctr  16222  bcmono  16223  bposlem1  16230  bposlem2  16231  bposlem3  16232  bposlem5  16234  lgslem3  16240  lgsdir2  16271  lgsdir  16273  lgsdilem2  16274  lgsdi  16275  gausslemma2dlem1a  16296  gausslemma2dlem3  16301  gausslemma2dlem6  16305  lgseisenlem3  16310  lgseisenlem4  16311  lgsquadlem1  16315  lgsquadlem2  16316  lgsquad2  16321  lgsquad3  16322  2lgslem1a1  16324  2lgslem1a  16326  2lgslem1c  16328  2sqlem2  16353  mul2sq  16354  2sqlem7  16359  usgredg2v  16584  ushgredgedg  16586  ushgredgedgloop  16588  uhgrissubgr  16621  vtxedgfi  16649  vtxlpfi  16650  wlkeq  16714  uspgr2wlkeq  16725  clwwlkccatlem  16760  clwwlkccat  16761  clwwlknccat  16783  bj-inex  17052  bj-bdfindis  17092  triap  17197  cvgcmp2nlemabs  17200  trilpolemisumle  17206  inffz  17241