Theorem adantrr 718

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ad2antrl  729  ad2ant2r  748  ad2ant2lr  749  cases2ALT  1049  consensus  1053  3adant3  1133  3ad2antr1  1190  reusv2lem3  5337  axprlem4OLD  5367  otsndisj  5467  otiunsndisj  5468  po2nr  5546  sotric  5562  sotrieq  5563  tz7.7  6343  fmptsnd  7117  fvtp1g  7146  f1cofveqaeqALT  7206  fsnex  7231  isocnv  7278  isores2  7281  isomin  7285  isoini  7286  f1oiso2  7300  ovmpodf  7516  offval  7633  ordsucun  7769  xp1st  7967  cnvf1olem  8053  fnse  8076  sexp2  8089  mpoxopoveq  8162  frrlem3  8231  frrlem13  8241  oalim  8460  omlim  8461  oaass  8489  omordi  8494  omwordri  8500  odi  8507  oen0  8515  oewordri  8521  nnawordi  8550  nnmordi  8560  omabs  8580  coflton  8600  nadd4  8627  erinxp  8731  dom2lem  8932  domssl  8938  mapen  9072  ssenen  9082  ssfiALT  9101  domfi  9116  php  9134  domunfican  9225  mapfien  9314  ordtypelem6  9431  ordtypelem7  9432  card2inf  9463  inf3lem6  9545  cantnfle  9583  cantnflem1b  9598  cantnflem1  9601  wemapwe  9609  ttrclselem2  9638  rankxplim3  9796  fseqenlem2  9938  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  cfsuc  10170  cfflb  10172  cofsmo  10182  infpssrlem4  10219  fin4en1  10222  ssfin4  10223  fin23lem26  10238  fin23lem22  10240  fin23lem27  10241  isf34lem4  10290  isf34lem5  10291  fin1a2lem12  10324  axdc3lem2  10364  axdc4lem  10368  ttukeylem6  10427  iundom2g  10453  pwcfsdom  10497  gchen2  10540  gchor  10541  fpwwe2lem6  10550  fpwwe2lem8  10552  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2  10557  pwfseqlem4  10576  gchina  10613  ltexprlem6  10955  prlem936  10961  mul4  11305  2addsub  11398  muladd  11573  ltleadd  11624  leord1  11668  eqord1  11669  ltord2  11670  leord2  11671  eqord2  11672  divmul3  11805  divcan7  11855  divadddiv  11861  lemul2a  12001  lemul12b  12003  ltmuldiv2  12021  ltdivmul  12022  ledivmul  12023  ltdivmul2  12024  lt2mul2div  12025  ledivmul2  12026  lemuldiv2  12028  lt2msq  12032  ltdiv23  12038  lediv23  12039  fimaxre  12091  supadd  12115  supmullem1  12117  cju  12146  zextlt  12594  suprzcl  12600  zmax  12886  xrlttr  13082  xrre3  13114  qbtwnre  13142  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  ixxdisj  13304  iooshf  13370  icodisj  13420  iccf1o  13440  modid  13846  modadd1  13858  modmul1  13877  seqf1o  13996  expsub  14063  sqlecan  14162  bcval5  14271  hashmap  14388  hashfacen  14407  seqcoll  14417  swrdswrdlem  14657  swrdccatin2  14682  cshwidxmod  14756  2cshwcshw  14778  cshwcshid  14780  resqreu  15205  lenegsq  15274  limsupbnd2  15436  icco1  15493  rlimresb  15518  rlimsqzlem  15602  rlimsqz  15603  rlimsqz2  15604  caucvgrlem  15626  fsum0diag2  15736  o1fsum  15767  ruclem8  16195  dvdsmulcr  16245  ndvdsadd  16370  bitsshft  16435  lcmdvds  16568  hashdvds  16736  eulerthlem2  16743  phisum  16752  pcqmul  16815  pcmpt  16854  prmreclem3  16880  4sqlem11  16917  0ram  16982  ramub1  16990  invfun  17722  initoeu2lem2  17973  coaval  18026  catcisolem  18068  funcestrcsetclem8  18104  fullestrcsetc  18108  embedsetcestrclem  18114  funcsetcestrclem8  18119  fullsetcestrc  18123  prfcl  18160  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  isposd  18279  lubun  18472  isacs3lem  18499  pslem  18529  psss  18537  chnccat  18583  chnpof1  18587  pwsdiagmhm  18790  grpinvid1  18958  grpinvid2  18959  grplcan  18967  grpnpncan0  19003  dfgrp3lem  19005  dfgrp3  19006  grplactcnv  19010  0nsg  19135  eqger  19144  eqg0subg  19162  qus0subgadd  19165  resghm  19198  conjghm  19215  subgga  19266  gaorber  19274  gastacl  19275  orbsta  19279  symgextf1lem  19386  psgnunilem2  19461  odid  19504  odmulg  19522  gexid  19547  odcau  19570  lsmssv  19609  lsmcom2  19621  pj1ghm  19669  frgpuptf  19736  frgpup1  19741  ghmplusg  19812  cyggex2  19863  gsumval3eu  19870  gsumval3  19873  ablfac1eu  20041  pgpfac1lem5  20047  ablsimpgfind  20078  ringurd  20157  srhmsubc  20648  isdomn4  20684  isdrngd  20733  isdrngdOLD  20735  issrngd  20823  lmhmf1o  21033  lmhmima  21034  lmhmpreima  21035  lspextmo  21043  pwssplit2  21047  pwssplit3  21048  lspdisj  21115  islbs3  21145  lbsextlem4  21151  drngnidl  21233  rngqiprngghmlem2  21278  rngqiprnglinlem1  21281  rngqiprngghm  21289  lidldvgen  21324  cnsubrg  21417  znunit  21553  cygznlem3  21559  dsmmsubg  21733  dsmmlss  21734  frlmsslsp  21786  frlmup1  21788  lindfrn  21811  f1lindf  21812  issubassa2  21882  psrbagconf1o  21919  psrgrp  21945  evlslem2  22067  mhplss  22131  psdmul  22142  psdmvr  22145  ply1sclf1  22264  mamuass  22377  dmatmul  22472  dmatsubcl  22473  dmatmulcl  22475  dmatcrng  22477  scmataddcl  22491  scmatsubcl  22492  scmatcrng  22496  mdetunilem2  22588  pm2mpf1  22774  pm2mpghm  22791  eltg2  22933  ntrss  23030  opncldf1  23059  ssnei2  23091  neindisj  23092  restopnb  23150  restntr  23157  tgcmp  23376  hauscmplem  23381  2ndc1stc  23426  2ndcdisj  23431  2ndcomap  23433  restlly  23458  lly1stc  23471  isref  23484  islocfin  23492  comppfsc  23507  txcls  23579  txdis1cn  23610  pthaus  23613  txlm  23623  qtoptop2  23674  qtopomap  23693  kqt0lem  23711  pt1hmeo  23781  ptuncnv  23782  xkocnv  23789  fbasfip  23843  fgabs  23854  fbasrn  23859  elfm2  23923  fmfnfmlem2  23930  fmfnfmlem4  23932  ptcmplem3  24029  ptcmplem4  24030  tsmsres  24119  tsmsxplem1  24128  utoptop  24209  elbl2ps  24364  elbl2  24365  blin  24396  xmeter  24408  xmetresbl  24412  stdbdxmet  24490  metrest  24499  metustexhalf  24531  dscmet  24547  nrmmetd  24549  tngngp2  24627  nmoi2  24705  icccmplem2  24799  reconnlem2  24803  metdstri  24827  metdsle  24828  metdsre  24829  metnrmlem3  24837  fsumcn  24847  icccvx  24927  bndth  24935  evth  24936  reparphti  24974  pi1blem  25016  tcphcph  25214  iscfil2  25243  cfilfcls  25251  iscau4  25256  iscauf  25257  caucfil  25260  cncmet  25299  minveclem7  25412  ovoliunlem1  25479  ovolicc2lem2  25495  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2lem5  25498  ovolicc2  25499  voliunlem3  25529  voliun  25531  ioombl  25542  volivth  25584  ismbfd  25616  ismbf3d  25631  itg1addlem1  25669  i1fadd  25672  itg1addlem4  25676  itg2split  25726  itg2monolem1  25727  itg2gt0  25737  ibllem  25741  itgvallem3  25763  iblposlem  25769  bddiblnc  25819  dvmptfsum  25952  rolle  25967  dvlip  25970  c1liplem1  25973  lhop1  25991  lhop2  25992  dvcvx  25997  dvfsumge  25999  dvfsumrlimge0  26007  dvfsumrlim  26008  dvfsum2  26011  mdegaddle  26049  mdegvscale  26050  mdegmullem  26053  ply1divex  26112  coeeulem  26199  plyco  26216  dgrlt  26241  vieta1  26289  ulmss  26375  ulmdvlem3  26380  iblulm  26385  tanord  26515  eff1olem  26525  logdivlt  26598  logccv  26640  lawcos  26793  xrlimcnp  26945  cxp2limlem  26953  cxp2lim  26954  cxploglim2  26956  divsqrtsumo1  26961  lgambdd  27014  sqff1o  27159  dvdsppwf1o  27163  dvdsflf1o  27164  musum  27168  muinv  27170  fsumdvdsmul  27172  sgmmul  27178  fsumvma  27190  logfac2  27194  chpchtsum  27196  logfacrlim  27201  logexprlim  27202  dchrelbas3  27215  dchrmulcl  27226  bposlem1  27261  lgsdchr  27332  lgsquadlem1  27357  lgsquadlem2  27358  lgsquad2lem2  27362  chebbnd1lem1  27446  chpchtlim  27456  rplogsumlem2  27462  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasum2lem  27473  dchrvmasumlem2  27475  dchrvmasumlem3  27476  dchrvmasumiflem2  27479  dchrisum0flb  27487  dchrisum0fno1  27488  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  rplogsum  27504  mulogsum  27509  mulog2sumlem2  27512  vmalogdivsum2  27515  2vmadivsumlem  27517  selberglem2  27523  selberg3lem1  27534  selberg4lem1  27537  selberg4  27538  pntrsumo1  27542  selberg34r  27548  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntibndlem3  27569  pntlemp  27587  ostthlem1  27604  ostth3  27615  ltsres  27640  noresle  27675  nosupno  27681  nosupbday  27683  noinfno  27696  bday1  27820  cutlt  27938  addsproplem2  27976  negsproplem2  28035  mulsuniflem  28155  mulsunif2lem  28175  precsexlem9  28221  precsexlem10  28222  precsexlem11  28223  om2noseqlt  28305  om2noseqlt2  28306  om2noseqf1o  28307  om2noseqrdg  28310  noseqrdgfn  28312  bdaypw2n0bndlem  28469  bdayfinbndlem1  28473  recut  28500  elreno2  28501  renegscl  28504  ercgrg  28599  oppperpex  28835  axlowdimlem15  29039  axlowdimlem16  29040  axcontlem10  29056  cusgrfilem1  29539  upgriswlk  29724  crctcshwlkn0  29904  wwlksnext  29976  wwlksnextwrd  29980  clwlkclwwlklem2a  30083  wwlksext2clwwlk  30142  grpoidinv  30594  grporcan  30604  grpoinvid1  30614  grpoinvid2  30615  grpolcan  30616  ablo4  30636  nvabs  30758  minvecolem7  30969  htthlem  31003  hvadd4  31122  hvaddsub4  31164  shscli  31403  pjspansn  31663  fh1  31704  fh2  31705  cm2j  31706  chscllem2  31724  spansncvi  31738  5oalem2  31741  5oalem5  31744  5oalem6  31745  3oalem2  31749  hoadd4  31870  cnvunop  32004  bralnfn  32034  eighmorth  32050  hmops  32106  hmopm  32107  adjlnop  32172  adjmul  32178  adjadd  32179  nmopcoi  32181  kbass5  32206  kbass6  32207  hstle  32316  stlesi  32327  mdsl0  32396  mdexchi  32421  atom1d  32439  superpos  32440  cvexchlem  32454  atomli  32468  atcvatlem  32471  chirredlem2  32477  chirredlem3  32478  atcvat4i  32483  mdsymlem1  32489  mdsymlem3  32491  mdsymlem5  32493  mdsymlem6  32494  sumdmdlem  32504  sumdmdlem2  32505  cdj1i  32519  opeldifid  32684  isoun  32790  1stpreimas  32794  f1od2  32807  indf1ofs  32941  ccatf1  33024  archirngz  33265  archiabllem1  33269  archiabllem2c  33271  qusxpid  33438  esum2d  34253  cntmeas  34386  ddemeas  34396  carsgclctunlem1  34477  itgeq12dv  34486  eulerpartlemgc  34522  eulerpartlemb  34528  eulerpartlemgs2  34540  ballotlemfc0  34653  ballotlemfcc  34654  reprss  34777  reprpmtf1o  34786  hgt750lemb  34816  bnj607  35074  fissorduni  35249  derangenlem  35369  subfacp1lem3  35380  subfacp1lem5  35382  cvmliftmolem2  35480  cvmliftlem6  35488  cvmlift2lem5  35505  cvmlift2lem7  35507  cvmlift2lem9  35509  mppspstlem  35769  dfon2lem6  35984  colinbtwnle  36316  finminlem  36516  nn0prpwlem  36520  isfne  36537  neibastop1  36557  neibastop2lem  36558  neibastop3  36560  tailfb  36575  onsuct0  36639  nndivsub  36655  mh-inf3f1  36739  knoppcnlem6  36774  knoppndvlem9  36796  knoppndvlem18  36805  knoppndvlem21  36808  bj-prmoore  37443  bj-finsumval0  37615  rdgeqoa  37700  pibt2  37747  lindsadd  37948  matunitlindflem2  37952  poimirlem4  37959  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem25  37980  poimirlem28  37983  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  mbfposadd  38002  itg2addnclem3  38008  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anc  38036  frinfm  38070  filbcmb  38075  seqpo  38082  sstotbnd2  38109  isbndx  38117  ssbnd  38123  prdsbnd  38128  ismtycnv  38137  ismtyres  38143  heiborlem3  38148  heibor  38156  ghomdiv  38227  grpokerinj  38228  isdrngo2  38293  rngohomco  38309  rngoisocnv  38316  rngoisoco  38317  crngm4  38338  crngohomfo  38341  isidlc  38350  ispridl2  38373  ispridlc  38405  prtlem16  39329  ax12eq  39401  ax12el  39402  lshpcmp  39448  omllaw3  39705  omlfh1N  39718  cvratlem  39881  cvrat3  39902  cvrat4  39903  ps-2  39938  elpaddn0  40260  paddasslem10  40289  cdleme0cp  40674  cdleme32a  40901  cdlemeg49lebilem  40999  cdleme50eq  41001  tendoeq2  41234  diaglbN  41515  diameetN  41516  diainN  41517  dvhopN  41576  djaclN  41596  djajN  41597  dihopelvalcpre  41708  dih1dimatlem  41789  dihmeetcl  41805  djhcl  41860  mapdpglem2  42133  3factsumint1  42474  sticksstones22  42621  unitscyglem4  42651  imacrhmcl  42973  frlmsnic  42999  psrmnd  43002  evlselvlem  43033  fsuppind  43037  0prjspn  43075  infdesc  43090  ismrc  43147  eldioph2  43208  lzenom  43216  rexrabdioph  43240  fphpdo  43263  irrapxlem3  43270  elpell14qr2  43308  pell14qrreccl  43310  pell14qrdich  43315  pellfundglb  43331  monotoddzzfi  43388  2nn0ind  43391  jm2.21  43440  jm2.22  43441  dnnumch3  43493  dnwech  43494  fnwe2lem2  43497  hbtlem6  43575  cantnfresb  43770  imo72b2lem1  44614  mnuprdlem1  44717  mnuprdlem2  44718  relpmin  45397  traxext  45422  cncmpmax  45481  disjf1  45631  eliccelioc  45969  fprodexp  46042  fprodabs2  46043  mullimc  46064  mullimcf  46071  islpcn  46085  limsuppnfdlem  46147  liminfval2  46214  xlimmnfvlem1  46278  xlimmnfvlem2  46279  xlimpnfvlem1  46282  xlimpnfvlem2  46283  cncfshift  46320  cncfperiod  46325  fprodcncf  46346  dvnprodlem1  46392  dvnprodlem2  46393  stoweidlem34  46480  stoweidlem48  46494  stoweidlem60  46506  fourierdlem42  46595  fourierdlem60  46612  fourierdlem61  46613  fourierdlem63  46615  fourierdlem65  46617  fourierdlem87  46639  fourierdlem97  46649  elaa2  46680  etransclem46  46726  etransc  46729  salrestss  46807  sge0iunmptlemfi  46859  isomennd  46977  ovnsslelem  47006  ovolval4lem2  47096  smflimlem3  47219  smflimlem4  47220  smflimlem6  47222  smfpimbor1lem1  47244  smflimmpt  47256  smflimsupmpt  47275  smfliminfmpt  47278  fsetsnf1  47512  fcoresf1  47529  fvelsetpreimafv  47859  icceuelpart  47908  prproropf1olem4  47978  fmtnoprmfac2  48042  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  gpg3nbgrvtx0ALT  48565  gpg3nbgrvtx1  48566  srhmsubcALTV  48813  xpco2  49344  catprs  49498  uppropd  49668  thincciso2  49942  prsthinc  49951  functermc  49995  fulltermc  49998  lmdran  50158  cmdlan  50159  aacllem  50288