Theorem adantrr 713

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 592	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 206  df-an 396

This theorem is referenced by:  ad2antrl  724  ad2ant2r  743  ad2ant2lr  744  cases2ALT  1045  consensus  1049  3adant3  1130  3ad2antr1  1186  reusv2lem3  5326  axprlem4  5352  otsndisj  5435  otiunsndisj  5436  po2nr  5516  sotric  5530  sotrieq  5531  tz7.7  6289  fmptsnd  7035  fvtp1g  7067  f1cofveqaeqALT  7126  fsnex  7148  isocnv  7194  isores2  7197  isomin  7201  isoini  7202  f1oiso2  7216  ovmpodf  7420  offval  7533  ordsucun  7660  xp1st  7849  cnvf1olem  7934  fnse  7958  mpoxopoveq  8019  frrlem3  8088  frrlem13  8098  wfrlem3OLD  8125  oalim  8338  omlim  8339  oaass  8368  omordi  8373  omwordri  8379  odi  8386  oen0  8393  oewordri  8399  nnawordi  8428  nnmordi  8438  omabs  8455  erinxp  8554  dom2lem  8751  mapen  8893  ssenen  8903  ssfiALT  8922  domfi  8940  php  8957  domunfican  9048  mapfien  9128  ordtypelem6  9243  ordtypelem7  9244  card2inf  9275  inf3lem6  9352  cantnfle  9390  cantnflem1b  9405  cantnflem1  9408  wemapwe  9416  ttrclselem2  9445  rankxplim3  9623  fseqenlem2  9765  dfac5lem4  9866  dfac2b  9870  cfsuc  9997  cfflb  9999  cofsmo  10009  infpssrlem4  10046  fin4en1  10049  ssfin4  10050  fin23lem26  10065  fin23lem22  10067  fin23lem27  10068  isf34lem4  10117  isf34lem5  10118  fin1a2lem12  10151  axdc3lem2  10191  axdc4lem  10195  ttukeylem6  10254  iundom2g  10280  pwcfsdom  10323  gchen2  10366  gchor  10367  fpwwe2lem6  10376  fpwwe2lem8  10378  fpwwe2lem10  10380  fpwwe2lem11  10381  fpwwe2  10383  pwfseqlem4  10402  gchina  10439  ltexprlem6  10781  prlem936  10787  mul4  11126  2addsub  11218  muladd  11390  ltleadd  11441  leord1  11485  eqord1  11486  ltord2  11487  leord2  11488  eqord2  11489  divmul3  11621  divcan7  11667  divadddiv  11673  lemul2a  11813  lemul12b  11815  ltmuldiv2  11832  ltdivmul  11833  ledivmul  11834  ltdivmul2  11835  lt2mul2div  11836  ledivmul2  11837  lemuldiv2  11839  lt2msq  11843  ltdiv23  11849  lediv23  11850  fimaxre  11902  supadd  11926  supmullem1  11928  cju  11952  zextlt  12377  suprzcl  12383  zmax  12667  xrlttr  12856  xrre3  12887  qbtwnre  12915  xrsupsslem  13023  xrinfmsslem  13024  supxrunb1  13035  supxrunb2  13036  ixxdisj  13076  iooshf  13140  icodisj  13190  iccf1o  13210  modid  13597  modadd1  13609  modmul1  13625  seqf1o  13745  expsub  13812  sqlecan  13906  bcval5  14013  hashmap  14131  hashfacen  14147  hashfacenOLD  14148  seqcoll  14159  swrdswrdlem  14398  swrdccatin2  14423  cshwidxmod  14497  2cshwcshw  14519  cshwcshid  14521  resqreu  14945  lenegsq  15013  limsupbnd2  15173  icco1  15230  rlimresb  15255  rlimsqzlem  15341  rlimsqz  15342  rlimsqz2  15343  caucvgrlem  15365  fsum0diag2  15476  o1fsum  15506  ruclem8  15927  dvdsmulcr  15976  ndvdsadd  16100  bitsshft  16163  lcmdvds  16294  hashdvds  16457  eulerthlem2  16464  phisum  16472  pcqmul  16535  pcmpt  16574  prmreclem3  16600  4sqlem11  16637  0ram  16702  ramub1  16710  invfun  17457  initoeu2lem2  17711  coaval  17764  catcisolem  17806  funcestrcsetclem8  17845  fullestrcsetc  17849  embedsetcestrclem  17855  funcsetcestrclem8  17860  fullsetcestrc  17864  prfcl  17901  prf1st  17902  prf2nd  17903  1st2ndprf  17904  curfuncf  17937  isposd  18022  lubun  18214  isacs3lem  18241  pslem  18271  psss  18279  pwsdiagmhm  18450  gsumccatOLD  18460  grpinvid1  18611  grpinvid2  18612  grplcan  18618  grpnpncan0  18652  dfgrp3lem  18654  dfgrp3  18655  grplactcnv  18659  0nsg  18778  eqger  18787  resghm  18831  conjghm  18846  subgga  18887  gaorber  18895  gastacl  18896  orbsta  18900  symgextf1lem  19009  psgnunilem2  19084  odid  19127  odmulg  19144  gexid  19167  odcau  19190  lsmssv  19229  lsmcom2  19241  pj1ghm  19290  frgpuptf  19357  frgpup1  19362  ghmplusg  19428  cyggex2  19479  gsumval3eu  19486  gsumval3  19489  ablfac1eu  19657  pgpfac1lem5  19663  ablsimpgfind  19694  isdrngd  19997  issrngd  20102  lmhmf1o  20289  lmhmima  20290  lmhmpreima  20291  lspextmo  20299  pwssplit2  20303  pwssplit3  20304  lspdisj  20368  islbs3  20398  lbsextlem4  20404  drngnidl  20481  lidldvgen  20507  cnsubrg  20639  znunit  20752  cygznlem3  20758  dsmmsubg  20931  dsmmlss  20932  frlmsslsp  20984  frlmup1  20986  lindfrn  21009  f1lindf  21010  issubassa2  21077  psrbagconf1o  21120  psrbagconf1oOLD  21121  evlslem2  21270  mhplss  21326  ply1sclf1  21441  mamuass  21530  dmatmul  21627  dmatsubcl  21628  dmatmulcl  21630  dmatcrng  21632  scmataddcl  21646  scmatsubcl  21647  scmatcrng  21651  mdetunilem2  21743  pm2mpf1  21929  pm2mpghm  21946  eltg2  22089  ntrss  22187  opncldf1  22216  ssnei2  22248  neindisj  22249  restopnb  22307  restntr  22314  tgcmp  22533  hauscmplem  22538  2ndc1stc  22583  2ndcdisj  22588  2ndcomap  22590  restlly  22615  lly1stc  22628  isref  22641  islocfin  22649  comppfsc  22664  txcls  22736  txdis1cn  22767  pthaus  22770  txlm  22780  qtoptop2  22831  qtopomap  22850  kqt0lem  22868  pt1hmeo  22938  ptuncnv  22939  xkocnv  22946  fbasfip  23000  fgabs  23011  fbasrn  23016  elfm2  23080  fmfnfmlem2  23087  fmfnfmlem4  23089  ptcmplem3  23186  ptcmplem4  23187  tsmsres  23276  tsmsxplem1  23285  utoptop  23367  elbl2ps  23523  elbl2  23524  blin  23555  xmeter  23567  xmetresbl  23571  stdbdxmet  23652  metrest  23661  metustexhalf  23693  dscmet  23709  nrmmetd  23711  tngngp2  23797  nmoi2  23875  icccmplem2  23967  reconnlem2  23971  metdstri  23995  metdsle  23996  metdsre  23997  metnrmlem3  24005  fsumcn  24014  icccvx  24094  bndth  24102  evth  24103  reparphti  24141  pi1blem  24183  tcphcph  24382  iscfil2  24411  cfilfcls  24419  iscau4  24424  iscauf  24425  caucfil  24428  cncmet  24467  minveclem7  24580  ovoliunlem1  24647  ovolicc2lem2  24663  ovolicc2lem3  24664  ovolicc2lem4  24665  ovolicc2lem5  24666  ovolicc2  24667  voliunlem3  24697  voliun  24699  ioombl  24710  volivth  24752  ismbfd  24784  ismbf3d  24799  itg1addlem1  24837  i1fadd  24840  itg1addlem4  24844  itg1addlem4OLD  24845  itg2split  24895  itg2monolem1  24896  itg2gt0  24906  ibllem  24910  itgvallem3  24931  iblposlem  24937  bddiblnc  24987  dvmptfsum  25120  rolle  25135  dvlip  25138  c1liplem1  25141  lhop1  25159  lhop2  25160  dvcvx  25165  dvfsumge  25167  dvfsumrlimge0  25175  dvfsumrlim  25176  dvfsum2  25179  mdegaddle  25220  mdegvscale  25221  mdegmullem  25224  ply1divex  25282  coeeulem  25366  plyco  25383  dgrlt  25408  vieta1  25453  ulmss  25537  ulmdvlem3  25542  iblulm  25547  tanord  25675  eff1olem  25685  logdivlt  25757  logccv  25799  lawcos  25947  xrlimcnp  26099  cxp2limlem  26106  cxp2lim  26107  cxploglim2  26109  divsqrtsumo1  26114  lgambdd  26167  sqff1o  26312  dvdsppwf1o  26316  dvdsflf1o  26317  musum  26321  muinv  26323  fsumdvdsmul  26325  sgmmul  26330  fsumvma  26342  logfac2  26346  chpchtsum  26348  logfacrlim  26353  logexprlim  26354  dchrelbas3  26367  dchrmulcl  26378  bposlem1  26413  lgsdchr  26484  lgsquadlem1  26509  lgsquadlem2  26510  lgsquad2lem2  26514  chebbnd1lem1  26598  chpchtlim  26608  rplogsumlem2  26614  dchrmusum2  26623  dchrvmasumlem1  26624  dchrvmasum2lem  26625  dchrvmasumlem2  26627  dchrvmasumlem3  26628  dchrvmasumiflem2  26631  dchrisum0flb  26639  dchrisum0fno1  26640  rpvmasum2  26641  dchrisum0re  26642  dchrisum0lem1  26645  dchrisum0lem2a  26646  dchrisum0lem2  26647  dchrisum0lem3  26648  rplogsum  26656  mulogsum  26661  mulog2sumlem2  26664  vmalogdivsum2  26667  2vmadivsumlem  26669  selberglem2  26675  selberg3lem1  26686  selberg4lem1  26689  selberg4  26690  pntrsumo1  26694  selberg34r  26700  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntibndlem3  26721  pntlemp  26739  ostthlem1  26756  ostth3  26767  ercgrg  26859  oppperpex  27095  axlowdimlem15  27305  axlowdimlem16  27306  axcontlem10  27322  cusgrfilem1  27803  upgriswlk  27988  crctcshwlkn0  28165  wwlksnext  28237  wwlksnextwrd  28241  clwlkclwwlklem2a  28341  wwlksext2clwwlk  28400  grpoidinv  28849  grporcan  28859  grpoinvid1  28869  grpoinvid2  28870  grpolcan  28871  ablo4  28891  nvabs  29013  minvecolem7  29224  htthlem  29258  hvadd4  29377  hvaddsub4  29419  shscli  29658  pjspansn  29918  fh1  29959  fh2  29960  cm2j  29961  chscllem2  29979  spansncvi  29993  5oalem2  29996  5oalem5  29999  5oalem6  30000  3oalem2  30004  hoadd4  30125  cnvunop  30259  bralnfn  30289  eighmorth  30305  hmops  30361  hmopm  30362  adjlnop  30427  adjmul  30433  adjadd  30434  nmopcoi  30436  kbass5  30461  kbass6  30462  hstle  30571  stlesi  30582  mdsl0  30651  mdexchi  30676  atom1d  30694  superpos  30695  cvexchlem  30709  atomli  30723  atcvatlem  30726  chirredlem2  30732  chirredlem3  30733  atcvat4i  30738  mdsymlem1  30744  mdsymlem3  30746  mdsymlem5  30748  mdsymlem6  30749  sumdmdlem  30759  sumdmdlem2  30760  cdj1i  30774  opeldifid  30917  isoun  31013  1stpreimas  31017  f1od2  31035  ccatf1  31202  archirngz  31422  archiabllem1  31426  archiabllem2c  31428  rngurd  31461  qusxpid  31538  indf1ofs  31973  esum2d  32040  cntmeas  32173  ddemeas  32183  carsgclctunlem1  32263  itgeq12dv  32272  eulerpartlemgc  32308  eulerpartlemb  32314  eulerpartlemgs2  32326  ballotlemfc0  32438  ballotlemfcc  32439  reprss  32576  reprpmtf1o  32585  hgt750lemb  32615  bnj607  32875  derangenlem  33112  subfacp1lem3  33123  subfacp1lem5  33125  cvmliftmolem2  33223  cvmliftlem6  33231  cvmlift2lem5  33248  cvmlift2lem7  33250  cvmlift2lem9  33252  mppspstlem  33512  dfon2lem6  33743  sexp2  33772  sltres  33844  noresle  33879  nosupno  33885  nosupbday  33887  noinfno  33900  bday1s  34004  colinbtwnle  34399  finminlem  34486  nn0prpwlem  34490  isfne  34507  neibastop1  34527  neibastop2lem  34528  neibastop3  34530  tailfb  34545  onsuct0  34609  nndivsub  34625  knoppcnlem6  34657  knoppndvlem9  34679  knoppndvlem18  34688  knoppndvlem21  34691  bj-prmoore  35265  bj-finsumval0  35435  rdgeqoa  35520  pibt2  35567  lindsadd  35749  matunitlindflem2  35753  poimirlem4  35760  poimirlem11  35767  poimirlem12  35768  poimirlem13  35769  poimirlem25  35781  poimirlem28  35784  heicant  35791  mblfinlem2  35794  mblfinlem3  35795  mblfinlem4  35796  mbfposadd  35803  itg2addnclem3  35809  ftc1anclem5  35833  ftc1anclem6  35834  ftc1anclem7  35835  ftc1anc  35837  frinfm  35872  filbcmb  35877  seqpo  35884  sstotbnd2  35911  isbndx  35919  ssbnd  35925  prdsbnd  35930  ismtycnv  35939  ismtyres  35945  heiborlem3  35950  heibor  35958  ghomdiv  36029  grpokerinj  36030  isdrngo2  36095  rngohomco  36111  rngoisocnv  36118  rngoisoco  36119  crngm4  36140  crngohomfo  36143  isidlc  36152  ispridl2  36175  ispridlc  36207  prtlem16  36862  ax12eq  36934  ax12el  36935  lshpcmp  36981  omllaw3  37238  omlfh1N  37251  cvratlem  37414  cvrat3  37435  cvrat4  37436  ps-2  37471  elpaddn0  37793  paddasslem10  37822  cdleme0cp  38207  cdleme32a  38434  cdlemeg49lebilem  38532  cdleme50eq  38534  tendoeq2  38767  diaglbN  39048  diameetN  39049  diainN  39050  dvhopN  39109  djaclN  39129  djajN  39130  dihopelvalcpre  39241  dih1dimatlem  39322  dihmeetcl  39338  djhcl  39393  mapdpglem2  39666  3factsumint1  40009  sticksstones22  40104  metakunt2  40106  isdomn4  40152  frlmsnic  40243  fsuppind  40259  mhphf  40265  0prjspn  40445  prjcrv0  40450  infdesc  40460  ismrc  40503  eldioph2  40564  lzenom  40572  rexrabdioph  40596  fphpdo  40619  irrapxlem3  40626  elpell14qr2  40664  pell14qrreccl  40666  pell14qrdich  40671  pellfundglb  40687  monotoddzzfi  40744  2nn0ind  40747  jm2.21  40796  jm2.22  40797  dnnumch3  40852  dnwech  40853  fnwe2lem2  40856  hbtlem6  40934  imo72b2lem1  41733  mnuprdlem1  41843  mnuprdlem2  41844  cncmpmax  42528  disjf1  42673  eliccelioc  43013  fprodexp  43089  fprodabs2  43090  mullimc  43111  mullimcf  43118  islpcn  43134  limsuppnfdlem  43196  liminfval2  43263  xlimmnfvlem1  43327  xlimmnfvlem2  43328  xlimpnfvlem1  43331  xlimpnfvlem2  43332  cncfshift  43369  cncfperiod  43374  fprodcncf  43395  dvnprodlem1  43441  dvnprodlem2  43442  stoweidlem34  43529  stoweidlem48  43543  stoweidlem60  43555  fourierdlem42  43644  fourierdlem60  43661  fourierdlem61  43662  fourierdlem63  43664  fourierdlem65  43666  fourierdlem87  43688  fourierdlem97  43698  elaa2  43729  etransclem46  43775  etransc  43778  sge0iunmptlemfi  43905  isomennd  44023  ovnsslelem  44052  ovolval4lem2  44142  ovolval5lem3  44146  smflimlem3  44259  smflimlem4  44260  smflimlem6  44262  smfpimbor1lem1  44283  smflimmpt  44294  smflimsupmpt  44313  smfliminfmpt  44316  fsetsnf1  44497  fcoresf1  44514  fvelsetpreimafv  44791  icceuelpart  44840  prproropf1olem4  44910  fmtnoprmfac2  44971  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  srhmsubc  45586  srhmsubcALTV  45604  catprs  46244  prsthinc  46287  aacllem  46457