Theorem adantrr 699

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 470	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 582	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  ad2ant2r  744  ad2ant2lr  745  cases2ALT  1062  consensus  1068  3adant3  1155  3ad2antr1  1232  reusv2lem3  5082  otsndisj  5187  otiunsndisj  5188  po2nr  5258  sotric  5271  sotrieq  5272  tz7.7  5976  fmptsnd  6670  fvtp1g  6698  f1cofveqaeqALT  6750  fsnex  6772  isocnv  6814  isores2  6817  isomin  6821  isoini  6822  f1oiso2  6836  ovmpt2df  7032  offval  7144  ordsucun  7265  xp1st  7440  1stconst  7509  cnvf1olem  7519  fnse  7538  mpt2xopoveq  7590  wfrlem3  7661  oalim  7859  omlim  7860  oaass  7888  omordi  7893  omwordri  7899  odi  7906  oen0  7913  oewordri  7919  nnawordi  7948  nnmordi  7958  omabs  7974  erinxp  8066  dom2lem  8242  mapen  8373  ssenen  8383  ssfi  8429  domfi  8430  domunfican  8482  mapfien  8562  ordtypelem6  8677  ordtypelem7  8678  card2inf  8709  inf3lem6  8787  cantnfle  8825  cantnflem1b  8840  cantnflem1  8843  wemapwe  8851  rankxplim3  9001  fseqenlem2  9141  dfac5lem4  9242  dfac2b  9246  dfac2OLD  9248  cfsuc  9374  cfflb  9376  cofsmo  9386  infpssrlem4  9423  fin4en1  9426  ssfin4  9427  fin23lem26  9442  fin23lem22  9444  fin23lem27  9445  isf34lem4  9494  isf34lem5  9495  fin1a2lem12  9528  axdc3lem2  9568  axdc4lem  9572  ttukeylem6  9631  iundom2g  9657  pwcfsdom  9700  gchen2  9743  gchor  9744  fpwwe2lem7  9753  fpwwe2lem9  9755  fpwwe2lem11  9757  fpwwe2lem12  9758  fpwwe2  9760  pwfseqlem4  9779  gchina  9816  ltexprlem6  10158  prlem936  10164  mul4  10500  2addsub  10590  muladd  10757  ltleadd  10806  leord1  10850  eqord1  10851  ltord2  10852  leord2  10853  eqord2  10854  divmul3  10985  divcan7  11029  divadddiv  11035  lemul2a  11173  lemul12b  11175  ltmuldiv2  11192  ltdivmul  11193  ledivmul  11194  ltdivmul2  11195  lt2mul2div  11196  ledivmul2  11197  lemuldiv2  11199  lt2msq  11203  ltdiv23  11209  lediv23  11210  supadd  11286  supmullem1  11288  cju  11311  zextlt  11737  suprzcl  11743  zmax  12024  xrlttr  12209  xrre3  12240  qbtwnre  12268  xrsupsslem  12375  xrinfmsslem  12376  supxrunb1  12387  supxrunb2  12388  ixxdisj  12428  iooshf  12490  icodisj  12538  iccf1o  12559  modid  12939  modadd1  12951  modmul1  12967  seqf1o  13085  expsub  13151  sqlecan  13214  bcval5  13345  hashmap  13459  hashfacen  13475  seqcoll  13485  swrdswrdlem  13703  cshwidxmod  13793  2cshwcshw  13815  cshwcshid  13817  resqreu  14236  lenegsq  14303  limsupbnd2  14457  icco1  14514  rlimresb  14539  rlimsqzlem  14622  rlimsqz  14623  rlimsqz2  14624  caucvgrlem  14646  fsum0diag2  14757  o1fsum  14787  ruclem8  15206  dvdsmulcr  15254  ndvdsadd  15373  bitsshft  15436  lcmdvds  15560  hashdvds  15717  eulerthlem2  15724  phisum  15732  pcqmul  15795  pcmpt  15833  prmreclem3  15859  4sqlem11  15896  0ram  15961  ramub1  15969  invfun  16648  initoeu2lem2  16889  coaval  16942  catcisolem  16980  funcestrcsetclem8  17012  fullestrcsetc  17016  embedsetcestrclem  17022  funcsetcestrclem8  17027  fullsetcestrc  17031  prfcl  17068  prf1st  17069  prf2nd  17070  1st2ndprf  17071  curfuncf  17103  isposd  17180  lubun  17348  isacs3lem  17391  pslem  17431  psss  17439  pwsdiagmhm  17594  gsumccat  17603  grpinvid1  17695  grpinvid2  17696  grplcan  17702  grpnpncan0  17736  dfgrp3lem  17738  dfgrp3  17739  grplactcnv  17743  0nsg  17861  eqger  17866  resghm  17898  conjghm  17913  subgga  17954  gaorber  17962  gastacl  17963  orbsta  17967  symgextf1lem  18061  psgnunilem2  18136  odid  18178  odmulg  18194  gexid  18217  odcau  18240  lsmssv  18279  lsmcom2  18291  pj1ghm  18337  frgpuptf  18404  frgpup1  18409  ghmplusg  18470  cyggex2  18519  gsumval3eu  18526  gsumval3  18529  ablfac1eu  18694  pgpfac1lem5  18700  isdrngd  18996  issrngd  19085  lmhmf1o  19273  lmhmima  19274  lmhmpreima  19275  lspextmo  19283  pwssplit2  19287  pwssplit3  19288  lspdisj  19352  islbs3  19384  lbsextlem4  19390  drngnidl  19458  lidldvgen  19484  issubassa2  19574  psrbagconf1o  19603  evlslem2  19740  ply1sclf1  19887  cnsubrg  20034  znunit  20139  cygznlem3  20145  dsmmsubg  20318  dsmmlss  20319  frlmsslsp  20366  frlmup1  20368  lindfrn  20391  f1lindf  20392  mamuass  20439  dmatmul  20535  dmatsubcl  20536  dmatmulcl  20538  dmatcrng  20540  scmataddcl  20554  scmatsubcl  20555  scmatcrng  20559  mdetunilem2  20651  pm2mpf1  20838  pm2mpghm  20855  eltg2  20997  ntrss  21094  opncldf1  21123  ssnei2  21155  neindisj  21156  restopnb  21214  restntr  21221  tgcmp  21439  hauscmplem  21444  2ndc1stc  21489  2ndcdisj  21494  2ndcomap  21496  restlly  21521  lly1stc  21534  isref  21547  islocfin  21555  comppfsc  21570  txcls  21642  txdis1cn  21673  pthaus  21676  txlm  21686  qtoptop2  21737  qtopomap  21756  kqt0lem  21774  pt1hmeo  21844  ptuncnv  21845  xkocnv  21852  fbasfip  21906  fgabs  21917  fbasrn  21922  elfm2  21986  fmfnfmlem2  21993  fmfnfmlem4  21995  ptcmplem3  22092  ptcmplem4  22093  tsmsres  22181  tsmsxplem1  22190  utoptop  22272  elbl2ps  22428  elbl2  22429  blin  22460  xmeter  22472  xmetresbl  22476  stdbdxmet  22554  metrest  22563  metustexhalf  22595  dscmet  22611  nrmmetd  22613  tngngp2  22690  nmoi2  22768  icccmplem2  22860  reconnlem2  22864  metdstri  22888  metdsle  22889  metdsre  22890  metnrmlem3  22898  fsumcn  22907  icccvx  22983  bndth  22991  evth  22992  reparphti  23030  pi1blem  23072  tchcph  23269  iscfil2  23298  cfilfcls  23306  iscau4  23311  iscauf  23312  caucfil  23315  cncmet  23353  minveclem7  23441  ovoliunlem1  23506  ovolicc2lem2  23522  ovolicc2lem3  23523  ovolicc2lem4  23524  ovolicc2lem5  23525  ovolicc2  23526  voliunlem3  23556  voliun  23558  ioombl  23569  volivth  23611  ismbfd  23643  ismbf3d  23658  itg1addlem1  23696  i1fadd  23699  itg1addlem4  23703  itg2seq  23746  itg2split  23753  itg2monolem1  23754  itg2gt0  23764  ibllem  23768  itgvallem3  23789  iblposlem  23795  dvmptfsum  23975  rolle  23990  dvlip  23993  c1liplem1  23996  lhop1  24014  lhop2  24015  dvcvx  24020  dvfsumge  24022  dvfsumrlimge0  24030  dvfsumrlim  24031  dvfsum2  24034  mdegaddle  24071  mdegvscale  24072  mdegmullem  24075  ply1divex  24133  coeeulem  24217  plyco  24234  dgrlt  24259  vieta1  24304  ulmss  24388  ulmdvlem3  24393  iblulm  24398  tanord  24522  eff1olem  24532  logdivlt  24604  logccv  24646  lawcos  24783  leibpilem1  24904  xrlimcnp  24932  cxp2limlem  24939  cxp2lim  24940  cxploglim2  24942  divsqrtsumo1  24947  lgambdd  25000  ftalem2  25037  sqff1o  25145  dvdsppwf1o  25149  dvdsflf1o  25150  musum  25154  muinv  25156  fsumdvdsmul  25158  sgmmul  25163  fsumvma  25175  logfac2  25179  chpchtsum  25181  logfacrlim  25186  logexprlim  25187  dchrelbas3  25200  dchrmulcl  25211  bposlem1  25246  lgsdchr  25317  lgsquadlem1  25342  lgsquadlem2  25343  lgsquad2lem2  25347  chebbnd1lem1  25395  chpchtlim  25405  rplogsumlem2  25411  dchrmusum2  25420  dchrvmasumlem1  25421  dchrvmasum2lem  25422  dchrvmasumlem2  25424  dchrvmasumlem3  25425  dchrvmasumiflem2  25428  dchrisum0flb  25436  dchrisum0fno1  25437  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lem1  25442  dchrisum0lem2a  25443  dchrisum0lem2  25444  dchrisum0lem3  25445  rplogsum  25453  mulogsum  25458  mulog2sumlem2  25461  vmalogdivsum2  25464  2vmadivsumlem  25466  selberglem2  25472  selberg3lem1  25483  selberg4lem1  25486  selberg4  25487  pntrsumo1  25491  selberg34r  25497  pntrlog2bndlem1  25503  pntrlog2bndlem2  25504  pntrlog2bndlem3  25505  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  pntrlog2bndlem6  25509  pntibndlem3  25518  pntlemp  25536  ostthlem1  25553  ostth3  25564  ercgrg  25649  ishpg  25888  axlowdimlem15  26073  axlowdimlem16  26074  axcontlem10  26090  cusgrfilem1  26602  upgriswlk  26788  crctcshwlkn0  26965  wwlksnextwrd  27057  clwlkclwwlklem2a  27164  grpoidinv  27714  grporcan  27724  grpoinvid1  27734  grpoinvid2  27735  grpolcan  27736  ablo4  27756  nvabs  27878  sspphOLD  28061  minvecolem7  28090  htthlem  28125  hvadd4  28244  hvaddsub4  28286  shscli  28527  pjspansn  28787  fh1  28828  fh2  28829  cm2j  28830  chscllem2  28848  spansncvi  28862  5oalem2  28865  5oalem5  28868  5oalem6  28869  3oalem2  28873  hoadd4  28994  cnvunop  29128  bralnfn  29158  eighmorth  29174  hmops  29230  hmopm  29231  adjlnop  29296  adjmul  29302  adjadd  29303  nmopcoi  29305  kbass5  29330  kbass6  29331  hstle  29440  stlesi  29451  mdsl0  29520  mdexchi  29545  atom1d  29563  superpos  29564  cvexchlem  29578  atomli  29592  atcvatlem  29595  chirredlem2  29601  chirredlem3  29602  atcvat4i  29607  mdsymlem1  29613  mdsymlem3  29615  mdsymlem5  29617  mdsymlem6  29618  sumdmdlem  29628  sumdmdlem2  29629  cdj1i  29643  opeldifid  29760  isoun  29829  1stpreimas  29833  f1od2  29849  archirngz  30091  archiabllem1  30095  archiabllem2c  30097  rngurd  30136  indf1ofs  30436  esum2d  30503  cntmeas  30637  ddemeas  30647  carsgclctunlem1  30727  itgeq12dv  30736  eulerpartlemgc  30772  eulerpartlemb  30778  eulerpartlemgs2  30790  ballotlemfc0  30902  ballotlemfcc  30903  signstfvneq0  30997  reprss  31043  reprpmtf1o  31052  hgt750lemb  31082  bnj607  31331  derangenlem  31498  subfacp1lem3  31509  subfacp1lem5  31511  cvmliftmolem2  31609  cvmliftlem6  31617  cvmlift2lem5  31634  cvmlift2lem7  31636  cvmlift2lem9  31638  mppspstlem  31813  dfon2lem6  32035  frrlem3  32125  sltres  32158  noresle  32189  nosupno  32192  colinbtwnle  32568  finminlem  32655  nn0prpwlem  32660  isfne  32677  neibastop1  32697  neibastop2lem  32698  neibastop3  32700  tailfb  32715  onsuct0  32779  nndivsub  32795  knoppcnlem6  32827  knoppndvlem9  32850  knoppndvlem18  32859  knoppndvlem21  32862  bj-finsumval0  33483  rdgeqoa  33553  matunitlindflem2  33738  poimirlem4  33745  poimirlem11  33752  poimirlem12  33753  poimirlem13  33754  poimirlem25  33766  poimirlem28  33769  heicant  33776  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  mbfposadd  33788  itg2addnclem3  33794  bddiblnc  33811  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anc  33824  frinfm  33861  filbcmb  33866  seqpo  33873  sstotbnd2  33903  isbndx  33911  ssbnd  33917  prdsbnd  33922  ismtycnv  33931  ismtyres  33937  heiborlem3  33942  heibor  33950  ghomdiv  34021  grpokerinj  34022  isdrngo2  34087  rngohomco  34103  rngoisocnv  34110  rngoisoco  34111  crngm4  34132  crngohomfo  34135  isidlc  34144  ispridl2  34167  ispridlc  34199  prtlem16  34667  ax12eq  34739  ax12el  34740  lshpcmp  34787  omllaw3  35044  omlfh1N  35057  cvratlem  35220  cvrat3  35241  cvrat4  35242  ps-2  35277  elpaddn0  35599  paddasslem10  35628  cdleme0cp  36013  cdleme32a  36240  cdlemeg49lebilem  36338  cdleme50eq  36340  tendoeq2  36573  diaglbN  36854  diameetN  36855  diainN  36856  dvhopN  36915  djaclN  36935  djajN  36936  dihopelvalcpre  37047  dih1dimatlem  37128  dihmeetcl  37144  djhcl  37199  mapdpglem2  37472  ismrc  37784  eldioph2  37845  lzenom  37853  rexrabdioph  37878  fphpdo  37901  irrapxlem3  37908  elpell14qr2  37946  pell14qrreccl  37948  pell14qrdich  37953  pellfundglb  37969  monotoddzzfi  38026  2nn0ind  38029  jm2.21  38080  jm2.22  38081  dnnumch3  38136  dnwech  38137  fnwe2lem2  38140  hbtlem6  38218  imo72b2lem1  38989  cncmpmax  39703  disjf1  39876  eliccelioc  40246  fprodexp  40324  fprodabs2  40325  mullimc  40346  mullimcf  40353  islpcn  40369  limsuppnfdlem  40431  liminfval2  40498  xlimmnfvlem1  40556  xlimmnfvlem2  40557  xlimpnfvlem1  40560  xlimpnfvlem2  40561  cncfshift  40585  cncfperiod  40590  fprodcncf  40612  dvnprodlem1  40659  dvnprodlem2  40660  stoweidlem34  40748  stoweidlem48  40762  stoweidlem60  40774  fourierdlem42  40863  fourierdlem60  40880  fourierdlem61  40881  fourierdlem63  40883  fourierdlem65  40885  fourierdlem87  40907  fourierdlem97  40917  elaa2  40948  etransclem46  40994  etransc  40997  sge0iunmptlemfi  41127  isomennd  41245  ovnsslelem  41274  ovolval4lem2  41364  ovolval5lem3  41368  smflimlem3  41481  smflimlem4  41482  smflimlem6  41484  smfpimbor1lem1  41505  smflimmpt  41516  smflimsupmpt  41535  smfliminfmpt  41538  icceuelpart  41965  fmtnoprmfac2  42072  bgoldbtbndlem2  42287  bgoldbtbndlem3  42288  srhmsubc  42662  srhmsubcALTV  42680  aacllem  43136