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  5347  axprlem4OLD  5376  otsndisj  5475  otiunsndisj  5476  po2nr  5554  sotric  5570  sotrieq  5571  tz7.7  6351  fmptsnd  7125  fvtp1g  7154  f1cofveqaeqALT  7214  fsnex  7239  isocnv  7286  isores2  7289  isomin  7293  isoini  7294  f1oiso2  7308  ovmpodf  7524  offval  7641  ordsucun  7777  xp1st  7975  cnvf1olem  8062  fnse  8085  sexp2  8098  mpoxopoveq  8171  frrlem3  8240  frrlem13  8250  oalim  8469  omlim  8470  oaass  8498  omordi  8503  omwordri  8509  odi  8516  oen0  8524  oewordri  8530  nnawordi  8559  nnmordi  8569  omabs  8589  coflton  8609  nadd4  8636  erinxp  8740  dom2lem  8941  domssl  8947  mapen  9081  ssenen  9091  ssfiALT  9110  domfi  9125  php  9143  domunfican  9234  mapfien  9323  ordtypelem6  9440  ordtypelem7  9441  card2inf  9472  inf3lem6  9554  cantnfle  9592  cantnflem1b  9607  cantnflem1  9610  wemapwe  9618  ttrclselem2  9647  rankxplim3  9805  fseqenlem2  9947  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  cfsuc  10179  cfflb  10181  cofsmo  10191  infpssrlem4  10228  fin4en1  10231  ssfin4  10232  fin23lem26  10247  fin23lem22  10249  fin23lem27  10250  isf34lem4  10299  isf34lem5  10300  fin1a2lem12  10333  axdc3lem2  10373  axdc4lem  10377  ttukeylem6  10436  iundom2g  10462  pwcfsdom  10506  gchen2  10549  gchor  10550  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2  10566  pwfseqlem4  10585  gchina  10622  ltexprlem6  10964  prlem936  10970  mul4  11313  2addsub  11406  muladd  11581  ltleadd  11632  leord1  11676  eqord1  11677  ltord2  11678  leord2  11679  eqord2  11680  divmul3  11813  divcan7  11862  divadddiv  11868  lemul2a  12008  lemul12b  12010  ltmuldiv2  12028  ltdivmul  12029  ledivmul  12030  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  lt2msq  12039  ltdiv23  12045  lediv23  12046  fimaxre  12098  supadd  12122  supmullem1  12124  cju  12153  zextlt  12578  suprzcl  12584  zmax  12870  xrlttr  13066  xrre3  13098  qbtwnre  13126  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  ixxdisj  13288  iooshf  13354  icodisj  13404  iccf1o  13424  modid  13828  modadd1  13840  modmul1  13859  seqf1o  13978  expsub  14045  sqlecan  14144  bcval5  14253  hashmap  14370  hashfacen  14389  seqcoll  14399  swrdswrdlem  14639  swrdccatin2  14664  cshwidxmod  14738  2cshwcshw  14760  cshwcshid  14762  resqreu  15187  lenegsq  15256  limsupbnd2  15418  icco1  15475  rlimresb  15500  rlimsqzlem  15584  rlimsqz  15585  rlimsqz2  15586  caucvgrlem  15608  fsum0diag2  15718  o1fsum  15748  ruclem8  16174  dvdsmulcr  16224  ndvdsadd  16349  bitsshft  16414  lcmdvds  16547  hashdvds  16714  eulerthlem2  16721  phisum  16730  pcqmul  16793  pcmpt  16832  prmreclem3  16858  4sqlem11  16895  0ram  16960  ramub1  16968  invfun  17700  initoeu2lem2  17951  coaval  18004  catcisolem  18046  funcestrcsetclem8  18082  fullestrcsetc  18086  embedsetcestrclem  18092  funcsetcestrclem8  18097  fullsetcestrc  18101  prfcl  18138  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfuncf  18173  isposd  18257  lubun  18450  isacs3lem  18477  pslem  18507  psss  18515  chnccat  18561  chnpof1  18565  pwsdiagmhm  18768  grpinvid1  18933  grpinvid2  18934  grplcan  18942  grpnpncan0  18978  dfgrp3lem  18980  dfgrp3  18981  grplactcnv  18985  0nsg  19110  eqger  19119  eqg0subg  19137  qus0subgadd  19140  resghm  19173  conjghm  19190  subgga  19241  gaorber  19249  gastacl  19250  orbsta  19254  symgextf1lem  19361  psgnunilem2  19436  odid  19479  odmulg  19497  gexid  19522  odcau  19545  lsmssv  19584  lsmcom2  19596  pj1ghm  19644  frgpuptf  19711  frgpup1  19716  ghmplusg  19787  cyggex2  19838  gsumval3eu  19845  gsumval3  19848  ablfac1eu  20016  pgpfac1lem5  20022  ablsimpgfind  20053  ringurd  20132  srhmsubc  20625  isdomn4  20661  isdrngd  20710  isdrngdOLD  20712  issrngd  20800  lmhmf1o  21010  lmhmima  21011  lmhmpreima  21012  lspextmo  21020  pwssplit2  21024  pwssplit3  21025  lspdisj  21092  islbs3  21122  lbsextlem4  21128  drngnidl  21210  rngqiprngghmlem2  21255  rngqiprnglinlem1  21258  rngqiprngghm  21266  lidldvgen  21301  cnsubrg  21394  znunit  21530  cygznlem3  21536  dsmmsubg  21710  dsmmlss  21711  frlmsslsp  21763  frlmup1  21765  lindfrn  21788  f1lindf  21789  issubassa2  21860  psrbagconf1o  21897  psrgrp  21924  evlslem2  22046  mhplss  22110  psdmul  22121  psdmvr  22124  ply1sclf1  22243  mamuass  22358  dmatmul  22453  dmatsubcl  22454  dmatmulcl  22456  dmatcrng  22458  scmataddcl  22472  scmatsubcl  22473  scmatcrng  22477  mdetunilem2  22569  pm2mpf1  22755  pm2mpghm  22772  eltg2  22914  ntrss  23011  opncldf1  23040  ssnei2  23072  neindisj  23073  restopnb  23131  restntr  23138  tgcmp  23357  hauscmplem  23362  2ndc1stc  23407  2ndcdisj  23412  2ndcomap  23414  restlly  23439  lly1stc  23452  isref  23465  islocfin  23473  comppfsc  23488  txcls  23560  txdis1cn  23591  pthaus  23594  txlm  23604  qtoptop2  23655  qtopomap  23674  kqt0lem  23692  pt1hmeo  23762  ptuncnv  23763  xkocnv  23770  fbasfip  23824  fgabs  23835  fbasrn  23840  elfm2  23904  fmfnfmlem2  23911  fmfnfmlem4  23913  ptcmplem3  24010  ptcmplem4  24011  tsmsres  24100  tsmsxplem1  24109  utoptop  24190  elbl2ps  24345  elbl2  24346  blin  24377  xmeter  24389  xmetresbl  24393  stdbdxmet  24471  metrest  24480  metustexhalf  24512  dscmet  24528  nrmmetd  24530  tngngp2  24608  nmoi2  24686  icccmplem2  24780  reconnlem2  24784  metdstri  24808  metdsle  24809  metdsre  24810  metnrmlem3  24818  fsumcn  24829  icccvx  24916  bndth  24925  evth  24926  reparphti  24964  reparphtiOLD  24965  pi1blem  25007  tcphcph  25205  iscfil2  25234  cfilfcls  25242  iscau4  25247  iscauf  25248  caucfil  25251  cncmet  25290  minveclem7  25403  ovoliunlem1  25471  ovolicc2lem2  25487  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2lem5  25490  ovolicc2  25491  voliunlem3  25521  voliun  25523  ioombl  25534  volivth  25576  ismbfd  25608  ismbf3d  25623  itg1addlem1  25661  i1fadd  25664  itg1addlem4  25668  itg2split  25718  itg2monolem1  25719  itg2gt0  25729  ibllem  25733  itgvallem3  25755  iblposlem  25761  bddiblnc  25811  dvmptfsum  25947  rolle  25962  dvlip  25966  c1liplem1  25969  lhop1  25987  lhop2  25988  dvcvx  25993  dvfsumge  25996  dvfsumrlimge0  26005  dvfsumrlim  26006  dvfsum2  26009  mdegaddle  26047  mdegvscale  26048  mdegmullem  26051  ply1divex  26110  coeeulem  26197  plyco  26214  dgrlt  26240  vieta1  26288  ulmss  26374  ulmdvlem3  26379  iblulm  26384  tanord  26515  eff1olem  26525  logdivlt  26598  logccv  26640  lawcos  26794  xrlimcnp  26946  cxp2limlem  26954  cxp2lim  26955  cxploglim2  26957  divsqrtsumo1  26962  lgambdd  27015  sqff1o  27160  dvdsppwf1o  27164  dvdsflf1o  27165  musum  27169  muinv  27171  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  sgmmul  27180  fsumvma  27192  logfac2  27196  chpchtsum  27198  logfacrlim  27203  logexprlim  27204  dchrelbas3  27217  dchrmulcl  27228  bposlem1  27263  lgsdchr  27334  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem2  27364  chebbnd1lem1  27448  chpchtlim  27458  rplogsumlem2  27464  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem2  27481  dchrisum0flb  27489  dchrisum0fno1  27490  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  rplogsum  27506  mulogsum  27511  mulog2sumlem2  27514  vmalogdivsum2  27517  2vmadivsumlem  27519  selberglem2  27525  selberg3lem1  27536  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntibndlem3  27571  pntlemp  27589  ostthlem1  27606  ostth3  27617  ltsres  27642  noresle  27677  nosupno  27683  nosupbday  27685  noinfno  27698  bday1  27822  cutlt  27940  addsproplem2  27978  negsproplem2  28037  mulsuniflem  28157  mulsunif2lem  28177  precsexlem9  28223  precsexlem10  28224  precsexlem11  28225  om2noseqlt  28307  om2noseqlt2  28308  om2noseqf1o  28309  om2noseqrdg  28312  noseqrdgfn  28314  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  recut  28502  elreno2  28503  renegscl  28506  ercgrg  28601  oppperpex  28837  axlowdimlem15  29041  axlowdimlem16  29042  axcontlem10  29058  cusgrfilem1  29541  upgriswlk  29726  crctcshwlkn0  29906  wwlksnext  29978  wwlksnextwrd  29982  clwlkclwwlklem2a  30085  wwlksext2clwwlk  30144  grpoidinv  30595  grporcan  30605  grpoinvid1  30615  grpoinvid2  30616  grpolcan  30617  ablo4  30637  nvabs  30759  minvecolem7  30970  htthlem  31004  hvadd4  31123  hvaddsub4  31165  shscli  31404  pjspansn  31664  fh1  31705  fh2  31706  cm2j  31707  chscllem2  31725  spansncvi  31739  5oalem2  31742  5oalem5  31745  5oalem6  31746  3oalem2  31750  hoadd4  31871  cnvunop  32005  bralnfn  32035  eighmorth  32051  hmops  32107  hmopm  32108  adjlnop  32173  adjmul  32179  adjadd  32180  nmopcoi  32182  kbass5  32207  kbass6  32208  hstle  32317  stlesi  32328  mdsl0  32397  mdexchi  32422  atom1d  32440  superpos  32441  cvexchlem  32455  atomli  32469  atcvatlem  32472  chirredlem2  32478  chirredlem3  32479  atcvat4i  32484  mdsymlem1  32490  mdsymlem3  32492  mdsymlem5  32494  mdsymlem6  32495  sumdmdlem  32505  sumdmdlem2  32506  cdj1i  32520  opeldifid  32685  isoun  32791  1stpreimas  32795  f1od2  32808  indf1ofs  32958  ccatf1  33041  archirngz  33282  archiabllem1  33286  archiabllem2c  33288  qusxpid  33455  esum2d  34270  cntmeas  34403  ddemeas  34413  carsgclctunlem1  34494  itgeq12dv  34503  eulerpartlemgc  34539  eulerpartlemb  34545  eulerpartlemgs2  34557  ballotlemfc0  34670  ballotlemfcc  34671  reprss  34794  reprpmtf1o  34803  hgt750lemb  34833  bnj607  35091  fissorduni  35265  derangenlem  35384  subfacp1lem3  35395  subfacp1lem5  35397  cvmliftmolem2  35495  cvmliftlem6  35503  cvmlift2lem5  35520  cvmlift2lem7  35522  cvmlift2lem9  35524  mppspstlem  35784  dfon2lem6  35999  colinbtwnle  36331  finminlem  36531  nn0prpwlem  36535  isfne  36552  neibastop1  36572  neibastop2lem  36573  neibastop3  36575  tailfb  36590  onsuct0  36654  nndivsub  36670  knoppcnlem6  36717  knoppndvlem9  36739  knoppndvlem18  36748  knoppndvlem21  36751  bj-prmoore  37365  bj-finsumval0  37537  rdgeqoa  37622  pibt2  37669  lindsadd  37861  matunitlindflem2  37865  poimirlem4  37872  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem25  37893  poimirlem28  37896  heicant  37903  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  mbfposadd  37915  itg2addnclem3  37921  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anc  37949  frinfm  37983  filbcmb  37988  seqpo  37995  sstotbnd2  38022  isbndx  38030  ssbnd  38036  prdsbnd  38041  ismtycnv  38050  ismtyres  38056  heiborlem3  38061  heibor  38069  ghomdiv  38140  grpokerinj  38141  isdrngo2  38206  rngohomco  38222  rngoisocnv  38229  rngoisoco  38230  crngm4  38251  crngohomfo  38254  isidlc  38263  ispridl2  38286  ispridlc  38318  prtlem16  39242  ax12eq  39314  ax12el  39315  lshpcmp  39361  omllaw3  39618  omlfh1N  39631  cvratlem  39794  cvrat3  39815  cvrat4  39816  ps-2  39851  elpaddn0  40173  paddasslem10  40202  cdleme0cp  40587  cdleme32a  40814  cdlemeg49lebilem  40912  cdleme50eq  40914  tendoeq2  41147  diaglbN  41428  diameetN  41429  diainN  41430  dvhopN  41489  djaclN  41509  djajN  41510  dihopelvalcpre  41621  dih1dimatlem  41702  dihmeetcl  41718  djhcl  41773  mapdpglem2  42046  3factsumint1  42388  sticksstones22  42535  unitscyglem4  42565  imacrhmcl  42881  frlmsnic  42907  psrmnd  42910  evlselvlem  42941  fsuppind  42945  0prjspn  42983  infdesc  42998  ismrc  43055  eldioph2  43116  lzenom  43124  rexrabdioph  43148  fphpdo  43171  irrapxlem3  43178  elpell14qr2  43216  pell14qrreccl  43218  pell14qrdich  43223  pellfundglb  43239  monotoddzzfi  43296  2nn0ind  43299  jm2.21  43348  jm2.22  43349  dnnumch3  43401  dnwech  43402  fnwe2lem2  43405  hbtlem6  43483  cantnfresb  43678  imo72b2lem1  44522  mnuprdlem1  44625  mnuprdlem2  44626  relpmin  45305  traxext  45330  cncmpmax  45389  disjf1  45539  eliccelioc  45878  fprodexp  45951  fprodabs2  45952  mullimc  45973  mullimcf  45980  islpcn  45994  limsuppnfdlem  46056  liminfval2  46123  xlimmnfvlem1  46187  xlimmnfvlem2  46188  xlimpnfvlem1  46191  xlimpnfvlem2  46192  cncfshift  46229  cncfperiod  46234  fprodcncf  46255  dvnprodlem1  46301  dvnprodlem2  46302  stoweidlem34  46389  stoweidlem48  46403  stoweidlem60  46415  fourierdlem42  46504  fourierdlem60  46521  fourierdlem61  46522  fourierdlem63  46524  fourierdlem65  46526  fourierdlem87  46548  fourierdlem97  46558  elaa2  46589  etransclem46  46635  etransc  46638  salrestss  46716  sge0iunmptlemfi  46768  isomennd  46886  ovnsslelem  46915  ovolval4lem2  47005  smflimlem3  47128  smflimlem4  47129  smflimlem6  47131  smfpimbor1lem1  47153  smflimmpt  47165  smflimsupmpt  47184  smfliminfmpt  47187  fsetsnf1  47409  fcoresf1  47426  fvelsetpreimafv  47744  icceuelpart  47793  prproropf1olem4  47863  fmtnoprmfac2  47924  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  gpgnbgrvtx0  48431  gpgnbgrvtx1  48432  gpg3nbgrvtx0ALT  48434  gpg3nbgrvtx1  48435  srhmsubcALTV  48682  xpco2  49213  catprs  49367  uppropd  49537  thincciso2  49811  prsthinc  49820  functermc  49864  fulltermc  49867  lmdran  50027  cmdlan  50028  aacllem  50157