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  5340  axprlem4OLD  5369  otsndisj  5462  otiunsndisj  5463  po2nr  5541  sotric  5557  sotrieq  5558  tz7.7  6337  fmptsnd  7109  fvtp1g  7138  f1cofveqaeqALT  7198  fsnex  7223  isocnv  7270  isores2  7273  isomin  7277  isoini  7278  f1oiso2  7292  ovmpodf  7508  offval  7625  ordsucun  7761  xp1st  7959  cnvf1olem  8046  fnse  8069  sexp2  8082  mpoxopoveq  8155  frrlem3  8224  frrlem13  8234  oalim  8453  omlim  8454  oaass  8482  omordi  8487  omwordri  8493  odi  8500  oen0  8507  oewordri  8513  nnawordi  8542  nnmordi  8552  omabs  8572  coflton  8592  nadd4  8619  erinxp  8721  dom2lem  8921  domssl  8927  mapen  9061  ssenen  9071  ssfiALT  9090  domfi  9105  php  9123  domunfican  9213  mapfien  9299  ordtypelem6  9416  ordtypelem7  9417  card2inf  9448  inf3lem6  9530  cantnfle  9568  cantnflem1b  9583  cantnflem1  9586  wemapwe  9594  ttrclselem2  9623  rankxplim3  9781  fseqenlem2  9923  dfac5lem4  10024  dfac5lem4OLD  10026  dfac2b  10029  cfsuc  10155  cfflb  10157  cofsmo  10167  infpssrlem4  10204  fin4en1  10207  ssfin4  10208  fin23lem26  10223  fin23lem22  10225  fin23lem27  10226  isf34lem4  10275  isf34lem5  10276  fin1a2lem12  10309  axdc3lem2  10349  axdc4lem  10353  ttukeylem6  10412  iundom2g  10438  pwcfsdom  10481  gchen2  10524  gchor  10525  fpwwe2lem6  10534  fpwwe2lem8  10536  fpwwe2lem10  10538  fpwwe2lem11  10539  fpwwe2  10541  pwfseqlem4  10560  gchina  10597  ltexprlem6  10939  prlem936  10945  mul4  11288  2addsub  11381  muladd  11556  ltleadd  11607  leord1  11651  eqord1  11652  ltord2  11653  leord2  11654  eqord2  11655  divmul3  11788  divcan7  11837  divadddiv  11843  lemul2a  11983  lemul12b  11985  ltmuldiv2  12003  ltdivmul  12004  ledivmul  12005  ltdivmul2  12006  lt2mul2div  12007  ledivmul2  12008  lemuldiv2  12010  lt2msq  12014  ltdiv23  12020  lediv23  12021  fimaxre  12073  supadd  12097  supmullem1  12099  cju  12128  zextlt  12553  suprzcl  12559  zmax  12845  xrlttr  13041  xrre3  13072  qbtwnre  13100  xrsupsslem  13208  xrinfmsslem  13209  supxrunb1  13220  supxrunb2  13221  ixxdisj  13262  iooshf  13328  icodisj  13378  iccf1o  13398  modid  13802  modadd1  13814  modmul1  13833  seqf1o  13952  expsub  14019  sqlecan  14118  bcval5  14227  hashmap  14344  hashfacen  14363  seqcoll  14373  swrdswrdlem  14613  swrdccatin2  14638  cshwidxmod  14712  2cshwcshw  14734  cshwcshid  14736  resqreu  15161  lenegsq  15230  limsupbnd2  15392  icco1  15449  rlimresb  15474  rlimsqzlem  15558  rlimsqz  15559  rlimsqz2  15560  caucvgrlem  15582  fsum0diag2  15692  o1fsum  15722  ruclem8  16148  dvdsmulcr  16198  ndvdsadd  16323  bitsshft  16388  lcmdvds  16521  hashdvds  16688  eulerthlem2  16695  phisum  16704  pcqmul  16767  pcmpt  16806  prmreclem3  16832  4sqlem11  16869  0ram  16934  ramub1  16942  invfun  17673  initoeu2lem2  17924  coaval  17977  catcisolem  18019  funcestrcsetclem8  18055  fullestrcsetc  18059  embedsetcestrclem  18065  funcsetcestrclem8  18070  fullsetcestrc  18074  prfcl  18111  prf1st  18112  prf2nd  18113  1st2ndprf  18114  curfuncf  18146  isposd  18230  lubun  18423  isacs3lem  18450  pslem  18480  psss  18488  chnccat  18534  chnpof1  18538  pwsdiagmhm  18741  grpinvid1  18906  grpinvid2  18907  grplcan  18915  grpnpncan0  18951  dfgrp3lem  18953  dfgrp3  18954  grplactcnv  18958  0nsg  19083  eqger  19092  eqg0subg  19110  qus0subgadd  19113  resghm  19146  conjghm  19163  subgga  19214  gaorber  19222  gastacl  19223  orbsta  19227  symgextf1lem  19334  psgnunilem2  19409  odid  19452  odmulg  19470  gexid  19495  odcau  19518  lsmssv  19557  lsmcom2  19569  pj1ghm  19617  frgpuptf  19684  frgpup1  19689  ghmplusg  19760  cyggex2  19811  gsumval3eu  19818  gsumval3  19821  ablfac1eu  19989  pgpfac1lem5  19995  ablsimpgfind  20026  ringurd  20105  srhmsubc  20597  isdomn4  20633  isdrngd  20682  isdrngdOLD  20684  issrngd  20772  lmhmf1o  20982  lmhmima  20983  lmhmpreima  20984  lspextmo  20992  pwssplit2  20996  pwssplit3  20997  lspdisj  21064  islbs3  21094  lbsextlem4  21100  drngnidl  21182  rngqiprngghmlem2  21227  rngqiprnglinlem1  21230  rngqiprngghm  21238  lidldvgen  21273  cnsubrg  21366  znunit  21502  cygznlem3  21508  dsmmsubg  21682  dsmmlss  21683  frlmsslsp  21735  frlmup1  21737  lindfrn  21760  f1lindf  21761  issubassa2  21831  psrbagconf1o  21868  psrgrp  21895  evlslem2  22015  mhplss  22071  psdmul  22082  psdmvr  22085  ply1sclf1  22204  mamuass  22318  dmatmul  22413  dmatsubcl  22414  dmatmulcl  22416  dmatcrng  22418  scmataddcl  22432  scmatsubcl  22433  scmatcrng  22437  mdetunilem2  22529  pm2mpf1  22715  pm2mpghm  22732  eltg2  22874  ntrss  22971  opncldf1  23000  ssnei2  23032  neindisj  23033  restopnb  23091  restntr  23098  tgcmp  23317  hauscmplem  23322  2ndc1stc  23367  2ndcdisj  23372  2ndcomap  23374  restlly  23399  lly1stc  23412  isref  23425  islocfin  23433  comppfsc  23448  txcls  23520  txdis1cn  23551  pthaus  23554  txlm  23564  qtoptop2  23615  qtopomap  23634  kqt0lem  23652  pt1hmeo  23722  ptuncnv  23723  xkocnv  23730  fbasfip  23784  fgabs  23795  fbasrn  23800  elfm2  23864  fmfnfmlem2  23871  fmfnfmlem4  23873  ptcmplem3  23970  ptcmplem4  23971  tsmsres  24060  tsmsxplem1  24069  utoptop  24150  elbl2ps  24305  elbl2  24306  blin  24337  xmeter  24349  xmetresbl  24353  stdbdxmet  24431  metrest  24440  metustexhalf  24472  dscmet  24488  nrmmetd  24490  tngngp2  24568  nmoi2  24646  icccmplem2  24740  reconnlem2  24744  metdstri  24768  metdsle  24769  metdsre  24770  metnrmlem3  24778  fsumcn  24789  icccvx  24876  bndth  24885  evth  24886  reparphti  24924  reparphtiOLD  24925  pi1blem  24967  tcphcph  25165  iscfil2  25194  cfilfcls  25202  iscau4  25207  iscauf  25208  caucfil  25211  cncmet  25250  minveclem7  25363  ovoliunlem1  25431  ovolicc2lem2  25447  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2lem5  25450  ovolicc2  25451  voliunlem3  25481  voliun  25483  ioombl  25494  volivth  25536  ismbfd  25568  ismbf3d  25583  itg1addlem1  25621  i1fadd  25624  itg1addlem4  25628  itg2split  25678  itg2monolem1  25679  itg2gt0  25689  ibllem  25693  itgvallem3  25715  iblposlem  25721  bddiblnc  25771  dvmptfsum  25907  rolle  25922  dvlip  25926  c1liplem1  25929  lhop1  25947  lhop2  25948  dvcvx  25953  dvfsumge  25956  dvfsumrlimge0  25965  dvfsumrlim  25966  dvfsum2  25969  mdegaddle  26007  mdegvscale  26008  mdegmullem  26011  ply1divex  26070  coeeulem  26157  plyco  26174  dgrlt  26200  vieta1  26248  ulmss  26334  ulmdvlem3  26339  iblulm  26344  tanord  26475  eff1olem  26485  logdivlt  26558  logccv  26600  lawcos  26754  xrlimcnp  26906  cxp2limlem  26914  cxp2lim  26915  cxploglim2  26917  divsqrtsumo1  26922  lgambdd  26975  sqff1o  27120  dvdsppwf1o  27124  dvdsflf1o  27125  musum  27129  muinv  27131  fsumdvdsmul  27133  fsumdvdsmulOLD  27135  sgmmul  27140  fsumvma  27152  logfac2  27156  chpchtsum  27158  logfacrlim  27163  logexprlim  27164  dchrelbas3  27177  dchrmulcl  27188  bposlem1  27223  lgsdchr  27294  lgsquadlem1  27319  lgsquadlem2  27320  lgsquad2lem2  27324  chebbnd1lem1  27408  chpchtlim  27418  rplogsumlem2  27424  dchrmusum2  27433  dchrvmasumlem1  27434  dchrvmasum2lem  27435  dchrvmasumlem2  27437  dchrvmasumlem3  27438  dchrvmasumiflem2  27441  dchrisum0flb  27449  dchrisum0fno1  27450  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem1  27455  dchrisum0lem2a  27456  dchrisum0lem2  27457  dchrisum0lem3  27458  rplogsum  27466  mulogsum  27471  mulog2sumlem2  27474  vmalogdivsum2  27477  2vmadivsumlem  27479  selberglem2  27485  selberg3lem1  27496  selberg4lem1  27499  selberg4  27500  pntrsumo1  27504  selberg34r  27510  pntrlog2bndlem1  27516  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntibndlem3  27531  pntlemp  27549  ostthlem1  27566  ostth3  27577  sltres  27602  noresle  27637  nosupno  27643  nosupbday  27645  noinfno  27658  bday1s  27776  cutlt  27877  addsproplem2  27914  negsproplem2  27972  mulsuniflem  28089  mulsunif2lem  28109  precsexlem9  28154  precsexlem10  28155  precsexlem11  28156  om2noseqlt  28230  om2noseqlt2  28231  om2noseqf1o  28232  om2noseqrdg  28235  noseqrdgfn  28237  recut  28399  renegscl  28401  ercgrg  28496  oppperpex  28732  axlowdimlem15  28936  axlowdimlem16  28937  axcontlem10  28953  cusgrfilem1  29436  upgriswlk  29621  crctcshwlkn0  29801  wwlksnext  29873  wwlksnextwrd  29877  clwlkclwwlklem2a  29980  wwlksext2clwwlk  30039  grpoidinv  30490  grporcan  30500  grpoinvid1  30510  grpoinvid2  30511  grpolcan  30512  ablo4  30532  nvabs  30654  minvecolem7  30865  htthlem  30899  hvadd4  31018  hvaddsub4  31060  shscli  31299  pjspansn  31559  fh1  31600  fh2  31601  cm2j  31602  chscllem2  31620  spansncvi  31634  5oalem2  31637  5oalem5  31640  5oalem6  31641  3oalem2  31645  hoadd4  31766  cnvunop  31900  bralnfn  31930  eighmorth  31946  hmops  32002  hmopm  32003  adjlnop  32068  adjmul  32074  adjadd  32075  nmopcoi  32077  kbass5  32102  kbass6  32103  hstle  32212  stlesi  32223  mdsl0  32292  mdexchi  32317  atom1d  32335  superpos  32336  cvexchlem  32350  atomli  32364  atcvatlem  32367  chirredlem2  32373  chirredlem3  32374  atcvat4i  32379  mdsymlem1  32385  mdsymlem3  32387  mdsymlem5  32389  mdsymlem6  32390  sumdmdlem  32400  sumdmdlem2  32401  cdj1i  32415  opeldifid  32581  isoun  32687  1stpreimas  32691  f1od2  32706  indf1ofs  32854  ccatf1  32937  archirngz  33165  archiabllem1  33169  archiabllem2c  33171  qusxpid  33335  esum2d  34127  cntmeas  34260  ddemeas  34270  carsgclctunlem1  34351  itgeq12dv  34360  eulerpartlemgc  34396  eulerpartlemb  34402  eulerpartlemgs2  34414  ballotlemfc0  34527  ballotlemfcc  34528  reprss  34651  reprpmtf1o  34660  hgt750lemb  34690  bnj607  34949  fissorduni  35122  derangenlem  35236  subfacp1lem3  35247  subfacp1lem5  35249  cvmliftmolem2  35347  cvmliftlem6  35355  cvmlift2lem5  35372  cvmlift2lem7  35374  cvmlift2lem9  35376  mppspstlem  35636  dfon2lem6  35851  colinbtwnle  36183  finminlem  36383  nn0prpwlem  36387  isfne  36404  neibastop1  36424  neibastop2lem  36425  neibastop3  36427  tailfb  36442  onsuct0  36506  nndivsub  36522  knoppcnlem6  36563  knoppndvlem9  36585  knoppndvlem18  36594  knoppndvlem21  36597  bj-prmoore  37180  bj-finsumval0  37350  rdgeqoa  37435  pibt2  37482  lindsadd  37673  matunitlindflem2  37677  poimirlem4  37684  poimirlem11  37691  poimirlem12  37692  poimirlem13  37693  poimirlem25  37705  poimirlem28  37708  heicant  37715  mblfinlem2  37718  mblfinlem3  37719  mblfinlem4  37720  mbfposadd  37727  itg2addnclem3  37733  ftc1anclem5  37757  ftc1anclem6  37758  ftc1anclem7  37759  ftc1anc  37761  frinfm  37795  filbcmb  37800  seqpo  37807  sstotbnd2  37834  isbndx  37842  ssbnd  37848  prdsbnd  37853  ismtycnv  37862  ismtyres  37868  heiborlem3  37873  heibor  37881  ghomdiv  37952  grpokerinj  37953  isdrngo2  38018  rngohomco  38034  rngoisocnv  38041  rngoisoco  38042  crngm4  38063  crngohomfo  38066  isidlc  38075  ispridl2  38098  ispridlc  38130  prtlem16  38988  ax12eq  39060  ax12el  39061  lshpcmp  39107  omllaw3  39364  omlfh1N  39377  cvratlem  39540  cvrat3  39561  cvrat4  39562  ps-2  39597  elpaddn0  39919  paddasslem10  39948  cdleme0cp  40333  cdleme32a  40560  cdlemeg49lebilem  40658  cdleme50eq  40660  tendoeq2  40893  diaglbN  41174  diameetN  41175  diainN  41176  dvhopN  41235  djaclN  41255  djajN  41256  dihopelvalcpre  41367  dih1dimatlem  41448  dihmeetcl  41464  djhcl  41519  mapdpglem2  41792  3factsumint1  42134  sticksstones22  42281  unitscyglem4  42311  imacrhmcl  42632  frlmsnic  42658  psrmnd  42663  evlselvlem  42704  fsuppind  42708  0prjspn  42746  infdesc  42761  ismrc  42818  eldioph2  42879  lzenom  42887  rexrabdioph  42911  fphpdo  42934  irrapxlem3  42941  elpell14qr2  42979  pell14qrreccl  42981  pell14qrdich  42986  pellfundglb  43002  monotoddzzfi  43059  2nn0ind  43062  jm2.21  43111  jm2.22  43112  dnnumch3  43164  dnwech  43165  fnwe2lem2  43168  hbtlem6  43246  cantnfresb  43441  imo72b2lem1  44286  mnuprdlem1  44389  mnuprdlem2  44390  relpmin  45069  traxext  45094  cncmpmax  45153  disjf1  45304  eliccelioc  45645  fprodexp  45718  fprodabs2  45719  mullimc  45740  mullimcf  45747  islpcn  45761  limsuppnfdlem  45823  liminfval2  45890  xlimmnfvlem1  45954  xlimmnfvlem2  45955  xlimpnfvlem1  45958  xlimpnfvlem2  45959  cncfshift  45996  cncfperiod  46001  fprodcncf  46022  dvnprodlem1  46068  dvnprodlem2  46069  stoweidlem34  46156  stoweidlem48  46170  stoweidlem60  46182  fourierdlem42  46271  fourierdlem60  46288  fourierdlem61  46289  fourierdlem63  46291  fourierdlem65  46293  fourierdlem87  46315  fourierdlem97  46325  elaa2  46356  etransclem46  46402  etransc  46405  salrestss  46483  sge0iunmptlemfi  46535  isomennd  46653  ovnsslelem  46682  ovolval4lem2  46772  smflimlem3  46895  smflimlem4  46896  smflimlem6  46898  smfpimbor1lem1  46920  smflimmpt  46932  smflimsupmpt  46951  smfliminfmpt  46954  fsetsnf1  47176  fcoresf1  47193  fvelsetpreimafv  47511  icceuelpart  47560  prproropf1olem4  47630  fmtnoprmfac2  47691  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  gpgnbgrvtx0  48198  gpgnbgrvtx1  48199  gpg3nbgrvtx0ALT  48201  gpg3nbgrvtx1  48202  srhmsubcALTV  48449  xpco2  48981  catprs  49136  uppropd  49306  thincciso2  49580  prsthinc  49589  functermc  49633  fulltermc  49636  lmdran  49796  cmdlan  49797  aacllem  49926