Theorem adantrr 717

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 593	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  728  ad2ant2r  747  ad2ant2lr  748  cases2ALT  1048  consensus  1052  3adant3  1132  3ad2antr1  1189  reusv2lem3  5338  axprlem4OLD  5367  otsndisj  5459  otiunsndisj  5460  po2nr  5538  sotric  5554  sotrieq  5555  tz7.7  6332  fmptsnd  7103  fvtp1g  7132  f1cofveqaeqALT  7192  fsnex  7217  isocnv  7264  isores2  7267  isomin  7271  isoini  7272  f1oiso2  7286  ovmpodf  7502  offval  7619  ordsucun  7755  xp1st  7953  cnvf1olem  8040  fnse  8063  sexp2  8076  mpoxopoveq  8149  frrlem3  8218  frrlem13  8228  oalim  8447  omlim  8448  oaass  8476  omordi  8481  omwordri  8487  odi  8494  oen0  8501  oewordri  8507  nnawordi  8536  nnmordi  8546  omabs  8566  coflton  8586  nadd4  8613  erinxp  8715  dom2lem  8914  domssl  8920  mapen  9054  ssenen  9064  ssfiALT  9083  domfi  9098  php  9116  domunfican  9206  mapfien  9292  ordtypelem6  9409  ordtypelem7  9410  card2inf  9441  inf3lem6  9523  cantnfle  9561  cantnflem1b  9576  cantnflem1  9579  wemapwe  9587  ttrclselem2  9616  rankxplim3  9771  fseqenlem2  9913  dfac5lem4  10014  dfac5lem4OLD  10016  dfac2b  10019  cfsuc  10145  cfflb  10147  cofsmo  10157  infpssrlem4  10194  fin4en1  10197  ssfin4  10198  fin23lem26  10213  fin23lem22  10215  fin23lem27  10216  isf34lem4  10265  isf34lem5  10266  fin1a2lem12  10299  axdc3lem2  10339  axdc4lem  10343  ttukeylem6  10402  iundom2g  10428  pwcfsdom  10471  gchen2  10514  gchor  10515  fpwwe2lem6  10524  fpwwe2lem8  10526  fpwwe2lem10  10528  fpwwe2lem11  10529  fpwwe2  10531  pwfseqlem4  10550  gchina  10587  ltexprlem6  10929  prlem936  10935  mul4  11278  2addsub  11371  muladd  11546  ltleadd  11597  leord1  11641  eqord1  11642  ltord2  11643  leord2  11644  eqord2  11645  divmul3  11778  divcan7  11827  divadddiv  11833  lemul2a  11973  lemul12b  11975  ltmuldiv2  11993  ltdivmul  11994  ledivmul  11995  ltdivmul2  11996  lt2mul2div  11997  ledivmul2  11998  lemuldiv2  12000  lt2msq  12004  ltdiv23  12010  lediv23  12011  fimaxre  12063  supadd  12087  supmullem1  12089  cju  12118  zextlt  12544  suprzcl  12550  zmax  12840  xrlttr  13036  xrre3  13067  qbtwnre  13095  xrsupsslem  13203  xrinfmsslem  13204  supxrunb1  13215  supxrunb2  13216  ixxdisj  13257  iooshf  13323  icodisj  13373  iccf1o  13393  modid  13797  modadd1  13809  modmul1  13828  seqf1o  13947  expsub  14014  sqlecan  14113  bcval5  14222  hashmap  14339  hashfacen  14358  seqcoll  14368  swrdswrdlem  14608  swrdccatin2  14633  cshwidxmod  14707  2cshwcshw  14729  cshwcshid  14731  resqreu  15156  lenegsq  15225  limsupbnd2  15387  icco1  15444  rlimresb  15469  rlimsqzlem  15553  rlimsqz  15554  rlimsqz2  15555  caucvgrlem  15577  fsum0diag2  15687  o1fsum  15717  ruclem8  16143  dvdsmulcr  16193  ndvdsadd  16318  bitsshft  16383  lcmdvds  16516  hashdvds  16683  eulerthlem2  16690  phisum  16699  pcqmul  16762  pcmpt  16801  prmreclem3  16827  4sqlem11  16864  0ram  16929  ramub1  16937  invfun  17668  initoeu2lem2  17919  coaval  17972  catcisolem  18014  funcestrcsetclem8  18050  fullestrcsetc  18054  embedsetcestrclem  18060  funcsetcestrclem8  18065  fullsetcestrc  18069  prfcl  18106  prf1st  18107  prf2nd  18108  1st2ndprf  18109  curfuncf  18141  isposd  18225  lubun  18418  isacs3lem  18445  pslem  18475  psss  18483  chnccat  18529  chnpof1  18533  pwsdiagmhm  18736  grpinvid1  18901  grpinvid2  18902  grplcan  18910  grpnpncan0  18946  dfgrp3lem  18948  dfgrp3  18949  grplactcnv  18953  0nsg  19079  eqger  19088  eqg0subg  19106  qus0subgadd  19109  resghm  19142  conjghm  19159  subgga  19210  gaorber  19218  gastacl  19219  orbsta  19223  symgextf1lem  19330  psgnunilem2  19405  odid  19448  odmulg  19466  gexid  19491  odcau  19514  lsmssv  19553  lsmcom2  19565  pj1ghm  19613  frgpuptf  19680  frgpup1  19685  ghmplusg  19756  cyggex2  19807  gsumval3eu  19814  gsumval3  19817  ablfac1eu  19985  pgpfac1lem5  19991  ablsimpgfind  20022  ringurd  20101  srhmsubc  20593  isdomn4  20629  isdrngd  20678  isdrngdOLD  20680  issrngd  20768  lmhmf1o  20978  lmhmima  20979  lmhmpreima  20980  lspextmo  20988  pwssplit2  20992  pwssplit3  20993  lspdisj  21060  islbs3  21090  lbsextlem4  21096  drngnidl  21178  rngqiprngghmlem2  21223  rngqiprnglinlem1  21226  rngqiprngghm  21234  lidldvgen  21269  cnsubrg  21362  znunit  21498  cygznlem3  21504  dsmmsubg  21678  dsmmlss  21679  frlmsslsp  21731  frlmup1  21733  lindfrn  21756  f1lindf  21757  issubassa2  21827  psrbagconf1o  21864  psrgrp  21891  evlslem2  22012  mhplss  22068  psdmul  22079  psdmvr  22082  ply1sclf1  22201  mamuass  22315  dmatmul  22410  dmatsubcl  22411  dmatmulcl  22413  dmatcrng  22415  scmataddcl  22429  scmatsubcl  22430  scmatcrng  22434  mdetunilem2  22526  pm2mpf1  22712  pm2mpghm  22729  eltg2  22871  ntrss  22968  opncldf1  22997  ssnei2  23029  neindisj  23030  restopnb  23088  restntr  23095  tgcmp  23314  hauscmplem  23319  2ndc1stc  23364  2ndcdisj  23369  2ndcomap  23371  restlly  23396  lly1stc  23409  isref  23422  islocfin  23430  comppfsc  23445  txcls  23517  txdis1cn  23548  pthaus  23551  txlm  23561  qtoptop2  23612  qtopomap  23631  kqt0lem  23649  pt1hmeo  23719  ptuncnv  23720  xkocnv  23727  fbasfip  23781  fgabs  23792  fbasrn  23797  elfm2  23861  fmfnfmlem2  23868  fmfnfmlem4  23870  ptcmplem3  23967  ptcmplem4  23968  tsmsres  24057  tsmsxplem1  24066  utoptop  24147  elbl2ps  24302  elbl2  24303  blin  24334  xmeter  24346  xmetresbl  24350  stdbdxmet  24428  metrest  24437  metustexhalf  24469  dscmet  24485  nrmmetd  24487  tngngp2  24565  nmoi2  24643  icccmplem2  24737  reconnlem2  24741  metdstri  24765  metdsle  24766  metdsre  24767  metnrmlem3  24775  fsumcn  24786  icccvx  24873  bndth  24882  evth  24883  reparphti  24921  reparphtiOLD  24922  pi1blem  24964  tcphcph  25162  iscfil2  25191  cfilfcls  25199  iscau4  25204  iscauf  25205  caucfil  25208  cncmet  25247  minveclem7  25360  ovoliunlem1  25428  ovolicc2lem2  25444  ovolicc2lem3  25445  ovolicc2lem4  25446  ovolicc2lem5  25447  ovolicc2  25448  voliunlem3  25478  voliun  25480  ioombl  25491  volivth  25533  ismbfd  25565  ismbf3d  25580  itg1addlem1  25618  i1fadd  25621  itg1addlem4  25625  itg2split  25675  itg2monolem1  25676  itg2gt0  25686  ibllem  25690  itgvallem3  25712  iblposlem  25718  bddiblnc  25768  dvmptfsum  25904  rolle  25919  dvlip  25923  c1liplem1  25926  lhop1  25944  lhop2  25945  dvcvx  25950  dvfsumge  25953  dvfsumrlimge0  25962  dvfsumrlim  25963  dvfsum2  25966  mdegaddle  26004  mdegvscale  26005  mdegmullem  26008  ply1divex  26067  coeeulem  26154  plyco  26171  dgrlt  26197  vieta1  26245  ulmss  26331  ulmdvlem3  26336  iblulm  26341  tanord  26472  eff1olem  26482  logdivlt  26555  logccv  26597  lawcos  26751  xrlimcnp  26903  cxp2limlem  26911  cxp2lim  26912  cxploglim2  26914  divsqrtsumo1  26919  lgambdd  26972  sqff1o  27117  dvdsppwf1o  27121  dvdsflf1o  27122  musum  27126  muinv  27128  fsumdvdsmul  27130  fsumdvdsmulOLD  27132  sgmmul  27137  fsumvma  27149  logfac2  27153  chpchtsum  27155  logfacrlim  27160  logexprlim  27161  dchrelbas3  27174  dchrmulcl  27185  bposlem1  27220  lgsdchr  27291  lgsquadlem1  27316  lgsquadlem2  27317  lgsquad2lem2  27321  chebbnd1lem1  27405  chpchtlim  27415  rplogsumlem2  27421  dchrmusum2  27430  dchrvmasumlem1  27431  dchrvmasum2lem  27432  dchrvmasumlem2  27434  dchrvmasumlem3  27435  dchrvmasumiflem2  27438  dchrisum0flb  27446  dchrisum0fno1  27447  rpvmasum2  27448  dchrisum0re  27449  dchrisum0lem1  27452  dchrisum0lem2a  27453  dchrisum0lem2  27454  dchrisum0lem3  27455  rplogsum  27463  mulogsum  27468  mulog2sumlem2  27471  vmalogdivsum2  27474  2vmadivsumlem  27476  selberglem2  27482  selberg3lem1  27493  selberg4lem1  27496  selberg4  27497  pntrsumo1  27501  selberg34r  27507  pntrlog2bndlem1  27513  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntrlog2bndlem6  27519  pntibndlem3  27528  pntlemp  27546  ostthlem1  27563  ostth3  27574  sltres  27599  noresle  27634  nosupno  27640  nosupbday  27642  noinfno  27655  bday1s  27773  cutlt  27874  addsproplem2  27911  negsproplem2  27969  mulsuniflem  28086  mulsunif2lem  28106  precsexlem9  28151  precsexlem10  28152  precsexlem11  28153  om2noseqlt  28227  om2noseqlt2  28228  om2noseqf1o  28229  om2noseqrdg  28232  noseqrdgfn  28234  recut  28396  renegscl  28398  ercgrg  28493  oppperpex  28729  axlowdimlem15  28932  axlowdimlem16  28933  axcontlem10  28949  cusgrfilem1  29432  upgriswlk  29617  crctcshwlkn0  29797  wwlksnext  29869  wwlksnextwrd  29873  clwlkclwwlklem2a  29973  wwlksext2clwwlk  30032  grpoidinv  30483  grporcan  30493  grpoinvid1  30503  grpoinvid2  30504  grpolcan  30505  ablo4  30525  nvabs  30647  minvecolem7  30858  htthlem  30892  hvadd4  31011  hvaddsub4  31053  shscli  31292  pjspansn  31552  fh1  31593  fh2  31594  cm2j  31595  chscllem2  31613  spansncvi  31627  5oalem2  31630  5oalem5  31633  5oalem6  31634  3oalem2  31638  hoadd4  31759  cnvunop  31893  bralnfn  31923  eighmorth  31939  hmops  31995  hmopm  31996  adjlnop  32061  adjmul  32067  adjadd  32068  nmopcoi  32070  kbass5  32095  kbass6  32096  hstle  32205  stlesi  32216  mdsl0  32285  mdexchi  32310  atom1d  32328  superpos  32329  cvexchlem  32343  atomli  32357  atcvatlem  32360  chirredlem2  32366  chirredlem3  32367  atcvat4i  32372  mdsymlem1  32378  mdsymlem3  32380  mdsymlem5  32382  mdsymlem6  32383  sumdmdlem  32393  sumdmdlem2  32394  cdj1i  32408  opeldifid  32574  isoun  32678  1stpreimas  32682  f1od2  32697  indf1ofs  32842  ccatf1  32925  archirngz  33153  archiabllem1  33157  archiabllem2c  33159  qusxpid  33323  esum2d  34101  cntmeas  34234  ddemeas  34244  carsgclctunlem1  34325  itgeq12dv  34334  eulerpartlemgc  34370  eulerpartlemb  34376  eulerpartlemgs2  34388  ballotlemfc0  34501  ballotlemfcc  34502  reprss  34625  reprpmtf1o  34634  hgt750lemb  34664  bnj607  34923  fissorduni  35096  derangenlem  35203  subfacp1lem3  35214  subfacp1lem5  35216  cvmliftmolem2  35314  cvmliftlem6  35322  cvmlift2lem5  35339  cvmlift2lem7  35341  cvmlift2lem9  35343  mppspstlem  35603  dfon2lem6  35821  colinbtwnle  36151  finminlem  36351  nn0prpwlem  36355  isfne  36372  neibastop1  36392  neibastop2lem  36393  neibastop3  36395  tailfb  36410  onsuct0  36474  nndivsub  36490  knoppcnlem6  36531  knoppndvlem9  36553  knoppndvlem18  36562  knoppndvlem21  36565  bj-prmoore  37148  bj-finsumval0  37318  rdgeqoa  37403  pibt2  37450  lindsadd  37652  matunitlindflem2  37656  poimirlem4  37663  poimirlem11  37670  poimirlem12  37671  poimirlem13  37672  poimirlem25  37684  poimirlem28  37687  heicant  37694  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  mbfposadd  37706  itg2addnclem3  37712  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anc  37740  frinfm  37774  filbcmb  37779  seqpo  37786  sstotbnd2  37813  isbndx  37821  ssbnd  37827  prdsbnd  37832  ismtycnv  37841  ismtyres  37847  heiborlem3  37852  heibor  37860  ghomdiv  37931  grpokerinj  37932  isdrngo2  37997  rngohomco  38013  rngoisocnv  38020  rngoisoco  38021  crngm4  38042  crngohomfo  38045  isidlc  38054  ispridl2  38077  ispridlc  38109  prtlem16  38907  ax12eq  38979  ax12el  38980  lshpcmp  39026  omllaw3  39283  omlfh1N  39296  cvratlem  39459  cvrat3  39480  cvrat4  39481  ps-2  39516  elpaddn0  39838  paddasslem10  39867  cdleme0cp  40252  cdleme32a  40479  cdlemeg49lebilem  40577  cdleme50eq  40579  tendoeq2  40812  diaglbN  41093  diameetN  41094  diainN  41095  dvhopN  41154  djaclN  41174  djajN  41175  dihopelvalcpre  41286  dih1dimatlem  41367  dihmeetcl  41383  djhcl  41438  mapdpglem2  41711  3factsumint1  42053  sticksstones22  42200  unitscyglem4  42230  imacrhmcl  42546  frlmsnic  42572  psrmnd  42577  evlselvlem  42618  fsuppind  42622  0prjspn  42660  infdesc  42675  ismrc  42733  eldioph2  42794  lzenom  42802  rexrabdioph  42826  fphpdo  42849  irrapxlem3  42856  elpell14qr2  42894  pell14qrreccl  42896  pell14qrdich  42901  pellfundglb  42917  monotoddzzfi  42974  2nn0ind  42977  jm2.21  43026  jm2.22  43027  dnnumch3  43079  dnwech  43080  fnwe2lem2  43083  hbtlem6  43161  cantnfresb  43356  imo72b2lem1  44201  mnuprdlem1  44304  mnuprdlem2  44305  relpmin  44984  traxext  45009  cncmpmax  45068  disjf1  45219  eliccelioc  45560  fprodexp  45633  fprodabs2  45634  mullimc  45655  mullimcf  45662  islpcn  45676  limsuppnfdlem  45738  liminfval2  45805  xlimmnfvlem1  45869  xlimmnfvlem2  45870  xlimpnfvlem1  45873  xlimpnfvlem2  45874  cncfshift  45911  cncfperiod  45916  fprodcncf  45937  dvnprodlem1  45983  dvnprodlem2  45984  stoweidlem34  46071  stoweidlem48  46085  stoweidlem60  46097  fourierdlem42  46186  fourierdlem60  46203  fourierdlem61  46204  fourierdlem63  46206  fourierdlem65  46208  fourierdlem87  46230  fourierdlem97  46240  elaa2  46271  etransclem46  46317  etransc  46320  salrestss  46398  sge0iunmptlemfi  46450  isomennd  46568  ovnsslelem  46597  ovolval4lem2  46687  smflimlem3  46810  smflimlem4  46811  smflimlem6  46813  smfpimbor1lem1  46835  smflimmpt  46847  smflimsupmpt  46866  smfliminfmpt  46869  fsetsnf1  47082  fcoresf1  47099  fvelsetpreimafv  47417  icceuelpart  47466  prproropf1olem4  47536  fmtnoprmfac2  47597  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  gpgnbgrvtx0  48104  gpgnbgrvtx1  48105  gpg3nbgrvtx0ALT  48107  gpg3nbgrvtx1  48108  srhmsubcALTV  48355  xpco2  48887  catprs  49042  uppropd  49212  thincciso2  49486  prsthinc  49495  functermc  49539  fulltermc  49542  lmdran  49702  cmdlan  49703  aacllem  49832