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  4147  opexg  4370  copsex2g  4388  ordin  4532  onin  4533  unexg  4591  eusv1  4600  opelvvg  4826  opthprc  4828  opbrop  4856  relop  4932  dmpropg  5263  unixpm  5326  funssres  5423  funinsn  5433  funtp  5437  fnco  5494  resasplitss  5572  fodmrnu  5626  relrnfvex  5716  funopdmsn  5898  fconst2g  5933  oveqan12d  6107  ovi3  6229  ovg  6231  f1opw2  6299  off  6319  offres  6372  suppfnss  6501  iunon  6559  nnsucsssuc  6769  nnaword1  6790  ertr  6826  erex  6835  brecop  6903  ecovdi  6924  ecovidi  6925  mapvalg  6936  pmvalg  6937  pmss12g  6960  mapsn  6977  en2sn  7107  xpf1o  7149  xpen  7150  phplem4  7161  ssfilem  7182  ssfilemd  7184  diffitest  7196  en1eqsn  7271  sbthlem7  7286  fsuppxpfi  7302  ordiso  7383  updjud  7429  fodju0  7494  finnum  7535  pr2nelem  7544  djucomen  7579  exmidontriimlem1  7584  2onetap  7628  ltsopi  7694  pitric  7695  pitri3or  7696  ltdcpi  7697  mulclpi  7702  addcompig  7703  mulcompig  7705  distrpig  7707  ltexpi  7711  ltapig  7712  ltmpig  7713  dfplpq2  7728  dfmpq2  7729  enqbreq2  7731  enqdc  7735  addcmpblnq  7741  addpipqqslem  7743  mulpipq2  7745  mulpipq  7746  mulpipqqs  7747  addclnq  7749  distrnqg  7761  ltdcnq  7771  ltrnqg  7794  enq0breq  7810  addclnq0  7825  nqnq0a  7828  nqnq0m  7829  nq0m0r  7830  distrnq0  7833  mulcomnq0  7834  genipv  7883  genplt2i  7884  genpelvl  7886  genpelvu  7887  addnqprlemrl  7931  addnqprlemru  7932  addnqprlemfl  7933  addnqprlemfu  7934  addnqpr  7935  mulnqprlemrl  7947  mulnqprlemru  7948  mulnqprlemfl  7949  mulnqprlemfu  7950  mulnqpr  7951  distrlem4prl  7958  distrlem4pru  7959  ltnqpr  7967  recexprlemloc  8005  archrecnq  8037  mulclsr  8128  1idsr  8142  00sr  8143  prsradd  8160  axmulass  8247  axdistr  8248  axcnre  8255  peano5nnnn  8266  mulrid  8330  axltadd  8402  lenlt  8408  cnegexlem3  8511  cnegex  8512  resubcl  8598  subeqrev  8710  muladd  8719  mulsub  8736  mulsub2  8737  ltaddsub2  8773  leaddsub2  8775  leltadd  8783  ltaddpos2  8789  posdif  8791  addge02  8809  mullt0  8816  recexre  8915  recextlem1  8988  recexap  8990  divmuldivap  9051  conjmulap  9068  div2subap  9176  prodgt02  9192  prodge02  9194  lemul2  9196  lemul2a  9198  ltmulgt12  9204  lemulge12  9206  ltmuldiv2  9214  ltdivmul2  9217  ledivmul2  9219  lemuldiv2  9221  negiso  9294  cju  9300  peano5nni  9317  nnaddcl  9334  nnmulcl  9335  nnsub  9353  addltmul  9554  avgle1  9558  avgle2  9559  nnrecl  9573  nn0nnaddcl  9606  zsubcl  9697  zleloe  9703  znnsub  9708  nzadd  9709  zmulcl  9710  zltp1le  9711  zleltp1  9712  nnleltp1  9716  nnltp1le  9717  nnaddm1cl  9718  nn0ltp1le  9719  nn0leltp1  9720  nn0ltlem1  9721  znn0sub  9722  nn0sub  9723  elz2  9728  zapne  9731  zdcle  9733  zdclt  9734  zltlen  9736  nn0lem1lt  9741  nnlem1lt  9742  nnltlem1  9743  zdiv  9746  zextle  9749  zextlt  9750  btwnnz  9752  prime  9757  nneo  9761  peano2uz2  9765  peano5uzti  9766  uzind  9769  fzind  9773  fnn0ind  9774  uzneg  9958  uz11  9962  eluzp1m1  9963  eluzp1p1  9965  uzin  9972  indstr  10010  uz2mulcl  10025  qre  10042  qaddcl  10052  qsubcl  10055  qltlen  10057  qlttri2  10058  irradd  10063  elpqb  10068  cnref1o  10069  rpaddcl  10096  rpmulcl  10097  rpdivcl  10098  rexadd  10272  rexsub  10273  xaddcom  10281  xnn0xadd0  10287  xnegdi  10288  elicc2  10358  iccshftr  10414  iccshftl  10416  iccdil  10418  icccntr  10420  fzval2  10432  elfz1eq  10457  peano2fzr  10459  fznlem  10463  fzsplit2  10473  fzsplit3  10476  fzaddel  10483  fzsubel  10484  fzrev2  10510  fzrev3  10512  uzsplit  10517  fzrevral  10530  fzrevral3  10532  fzshftral  10533  elfz2nn0  10537  fznn0sub2  10553  fz0fzdiffz0  10555  elfzmlbp  10557  difelfzle  10559  difelfznle  10560  1fv  10564  elfzouz2  10587  fzo0n  10593  fzouzsplit  10606  fzoun  10608  elfzo0le  10615  fzonmapblen  10617  fzofzim  10618  fzoaddel2  10626  eluzgtdifelfzo  10633  elfzodifsumelfzo  10637  ubmelm1fzo  10662  fzofzp1b  10664  fzosplitprm1  10671  fzostep1  10674  subfzo0  10679  zsupcllemstep  10680  qdclt  10698  qbtwnxr  10710  flqbi2  10748  divfl0  10753  flqzadd  10755  flqmulnn0  10756  addmodidr  10832  modfzo0difsn  10854  frec2uzltd  10862  frec2uzrand  10864  frecfzen2  10886  seqshft2g  10941  seq3split  10947  seqsplitg  10948  seq3caopr2  10952  seqcaopr2g  10953  seqf1oglem2  10979  exp3vallem  10999  expcllem  11009  expcl2lemap  11010  1exp  11027  expge1  11035  expadd  11040  expmul  11043  expsubap  11046  leexp1a  11053  lt2sq  11072  le2sq  11073  sumsqeq0  11077  qsqeqor  11109  bernneq  11120  bernneq2  11121  sq11ap  11167  facdiv  11199  faclbnd  11202  faclbnd3  11204  faclbnd6  11205  facavg  11207  bcrpcl  11214  bccmpl  11215  bcm1n  11230  fiubm  11294  seq3coll  11317  eqwrd  11368  ccatcl  11384  ccatclab  11385  ccatlen  11386  ccat0  11387  ccatval1  11388  ccatval2  11389  elfzelfzccat  11391  ccatvalfn  11392  ccatsymb  11393  ccatval21sw  11396  ccatrn  11400  lswccatn0lsw  11402  ccatalpha  11404  ccatrcl1  11405  swrdfv2  11458  swrdsbslen  11461  swrdspsleq  11462  swrdccat2  11466  pfxclz  11474  ccatpfx  11496  pfxccat1  11497  swrdswrdlem  11499  pfxswrd  11501  pfxccatin12lem4  11521  pfxccatin12lem1  11523  pfxccatin12lem2  11526  pfxccatin12lem3  11527  pfxccat3  11529  swrdccat  11530  pfxccatpfx2  11532  pfxccat3a  11533  swrdccat3blem  11534  swrdccat3b  11535  s2dmg  11585  shftfvalg  11606  shftf  11618  crre  11645  crim  11646  mulreap  11652  readd  11657  resub  11658  remul2  11661  imadd  11665  imsub  11666  immul2  11668  ipcnval  11674  cjsub  11680  cjreim  11692  caucvgre  11770  rexanuz  11777  rexuz3  11779  resqrexlemover  11799  resqrexlemcvg  11808  resqrexlemglsq  11811  sqrtle  11825  sqrtlt  11826  sqrt11ap  11827  sqrt11  11828  absreimsq  11856  absreim  11857  absmul  11858  sqabs  11872  absdiflt  11882  absdifle  11883  abssuble0  11893  abs2difabs  11898  fzomaxdif  11903  caubnd2  11907  rpmaxcl  12013  zmaxcl  12014  nn0maxcl  12015  minmax  12021  mincl  12022  min1inf  12023  min2inf  12024  minabs  12027  minclpr  12028  rpmincl  12029  zmincl  12030  2zinfmin  12035  xrmaxrecl  12047  xrminmax  12057  xrmincl  12058  xrmin1inf  12059  xrmin2inf  12060  xrminrecl  12065  xrminrpcl  12066  iooinsup  12069  climconst2  12083  climuni  12085  2clim  12093  climshft  12096  climshft2  12098  cjcn2  12108  climaddc1  12121  climmulc2  12123  climsubc1  12124  climsubc2  12125  climlec2  12133  summodclem2a  12174  zsumdc  12177  isumclim3  12216  mptfzshft  12235  fsumrev  12236  fisum0diag2  12240  telfsumo2  12260  fsumparts  12263  cvgcmpub  12269  binomlem  12276  binom1p  12278  binom1dif  12280  bcxmas  12282  isumshft  12283  expcnvap0  12295  expcnv  12297  geosergap  12299  geolim  12304  cvgratnnlemrate  12323  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  prodmodc  12371  zproddc  12372  fprodf1o  12381  fprodeq0  12410  efcj  12466  eftlub  12483  effsumlt  12485  efieq  12528  sinsub  12533  cossub  12534  subsin  12536  sinmul  12537  cosmul  12538  addcos  12539  subcos  12540  dvdssub2  12628  dvdsadd  12629  dvdsaddr  12630  dvdssub  12631  dvdssubr  12632  fzocongeq  12651  odd2np1  12666  opoe  12688  omoe  12689  opeo  12690  omeo  12691  divalgb  12718  ndvdsadd  12724  bitsfi  12750  gcdmndc  12758  gcdabs  12791  dvdsgcd  12815  absmulgcd  12820  gcdmultiple  12823  gcdmultiplez  12824  rpmulgcd  12829  sqgcd  12832  dvdssqlem  12833  dvdssq  12834  nninfctlemfo  12843  nn0seqcvgd  12845  ialgrlemconst  12847  algrf  12849  algrp1  12850  algcvg  12852  algcvga  12855  lcmval  12867  lcmabs  12880  lcmgcd  12882  lcmdvds  12883  lcmgcdnn  12886  coprmgcdb  12892  coprmdvds  12896  coprmdvds2  12897  qredeq  12900  isprm3  12922  nprm  12927  divgcdodd  12948  prmdvdsexp  12953  sqrt2irr  12967  zgcdsq  13007  hashdvds  13029  phiprmpw  13030  crth  13032  phimullem  13033  modprm0  13063  coprimeprodsq  13066  coprimeprodsq2  13067  pythagtriplem2  13075  pythagtriplem19  13091  pcdvdsb  13129  pcneg  13134  pc2dvds  13139  pc11  13140  pcmpt  13152  pcfac  13159  infpnlem1  13168  prmunb  13171  1arithlem4  13175  1arith  13176  gzaddcl  13186  gzmulcl  13187  gzreim  13188  gzsubcl  13189  4sqlem1  13197  4sqlem4a  13200  4sqlem4  13201  4sqlem12  13211  ballotfilemfc0  13291  ballotfilemfcc  13292  setsvalg  13441  setsfun0  13447  restval  13659  mndinvmod  13818  resmhm  13854  resmhm2  13855  mhmco  13857  dfgrp3m  13964  mhmmnd  13979  mulgnngzsum  13990  mulgnn0z  14012  mulgnndir  14014  ghmex  14118  0ghm  14121  resghm  14123  resghm2  14124  ghmco  14127  ghmeql  14130  kerf1ghm  14137  cntzmhm  14174  ablsubsub23  14220  xpsval  14309  dfrhm2  14571  isrhm  14575  rhmfn  14589  rhmval  14590  rhmco  14591  resrhm  14666  rhmeql  14668  rhmima  14669  lmodfopne  14773  lspf  14836  znidom  15102  znrrg  15105  issubassa3  15122  innei  15401  cnovex  15434  txuni2  15494  txbasex  15495  txbas  15496  txtop  15498  txtopon  15500  txss12  15504  txbasval  15505  txcnp  15509  upxp  15510  txcnmpt  15511  uptx  15512  txcn  15513  txrest  15514  txdis  15515  cnmpt21  15529  hmeoco  15554  txhmeo  15557  isxmet2d  15586  blin2  15670  comet  15737  metcn  15752  txmetcn  15757  qtopbasss  15759  qtopbas  15760  remetdval  15785  bl2ioo  15788  blssioo  15791  divcnap  15803  cncfmet  15830  dvaddxxbr  15939  dvcjbr  15946  plyf  15975  ply1termlem  15980  plymullem1  15986  plyaddlem  15987  plymullem  15988  plycolemc  15996  plyreres  16002  dvply1  16003  efle  16014  reapef  16016  sinperlem  16047  sincosq2sgn  16066  sincosq3sgn  16067  sincos6thpi  16081  ioocosf1o  16094  reaplog  16109  relogoprlem  16110  logleb  16117  cxple3  16168  cxpcom  16185  efnthr  16188  birthdaylem2  16238  birthdaylem3  16239  dvdsppwf1o  16295  fsumdvdsmul  16297  1sgmprm  16300  chtublem  16307  mersenne  16309  pcbcctr  16315  bcmono  16316  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem5  16327  bposlem6  16328  bposlem7  16329  lgslem3  16338  lgsdir2  16369  lgsdir  16371  lgsdilem2  16372  lgsdi  16373  gausslemma2dlem1a  16394  gausslemma2dlem3  16399  gausslemma2dlem6  16403  lgseisenlem3  16408  lgseisenlem4  16409  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2  16419  lgsquad3  16420  2lgslem1a1  16422  2lgslem1a  16424  2lgslem1c  16426  2sqlem2  16451  mul2sq  16452  2sqlem7  16457  usgredg2v  16682  ushgredgedg  16684  ushgredgedgloop  16686  uhgrissubgr  16719  vtxedgfi  16747  vtxlpfi  16748  wlkeq  16812  uspgr2wlkeq  16823  clwwlkccatlem  16858  clwwlkccat  16859  clwwlknccat  16881  bj-inex  17150  bj-bdfindis  17190  triap  17296  cvgcmp2nlemabs  17299  trilpolemisumle  17306  inffz  17341