Theorem adantrr 715

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad2antrl  726  ad2ant2r  745  ad2ant2lr  746  cases2ALT  1047  consensus  1051  3adant3  1132  3ad2antr1  1188  reusv2lem3  5398  axprlem4  5424  otsndisj  5519  otiunsndisj  5520  po2nr  5602  sotric  5616  sotrieq  5617  tz7.7  6390  fmptsnd  7169  fvtp1g  7201  f1cofveqaeqALT  7260  fsnex  7283  isocnv  7329  isores2  7332  isomin  7336  isoini  7337  f1oiso2  7351  ovmpodf  7566  offval  7681  ordsucun  7815  xp1st  8009  cnvf1olem  8098  fnse  8121  sexp2  8134  mpoxopoveq  8206  frrlem3  8275  frrlem13  8285  wfrlem3OLD  8312  oalim  8534  omlim  8535  oaass  8563  omordi  8568  omwordri  8574  odi  8581  oen0  8588  oewordri  8594  nnawordi  8623  nnmordi  8633  omabs  8652  coflton  8672  nadd4  8699  erinxp  8787  dom2lem  8990  domssl  8996  mapen  9143  ssenen  9153  ssfiALT  9176  domfi  9194  php  9212  domunfican  9322  mapfien  9405  ordtypelem6  9520  ordtypelem7  9521  card2inf  9552  inf3lem6  9630  cantnfle  9668  cantnflem1b  9683  cantnflem1  9686  wemapwe  9694  ttrclselem2  9723  rankxplim3  9878  fseqenlem2  10022  dfac5lem4  10123  dfac2b  10127  cfsuc  10254  cfflb  10256  cofsmo  10266  infpssrlem4  10303  fin4en1  10306  ssfin4  10307  fin23lem26  10322  fin23lem22  10324  fin23lem27  10325  isf34lem4  10374  isf34lem5  10375  fin1a2lem12  10408  axdc3lem2  10448  axdc4lem  10452  ttukeylem6  10511  iundom2g  10537  pwcfsdom  10580  gchen2  10623  gchor  10624  fpwwe2lem6  10633  fpwwe2lem8  10635  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2  10640  pwfseqlem4  10659  gchina  10696  ltexprlem6  11038  prlem936  11044  mul4  11386  2addsub  11478  muladd  11650  ltleadd  11701  leord1  11745  eqord1  11746  ltord2  11747  leord2  11748  eqord2  11749  divmul3  11881  divcan7  11927  divadddiv  11933  lemul2a  12073  lemul12b  12075  ltmuldiv2  12092  ltdivmul  12093  ledivmul  12094  ltdivmul2  12095  lt2mul2div  12096  ledivmul2  12097  lemuldiv2  12099  lt2msq  12103  ltdiv23  12109  lediv23  12110  fimaxre  12162  supadd  12186  supmullem1  12188  cju  12212  zextlt  12640  suprzcl  12646  zmax  12933  xrlttr  13123  xrre3  13154  qbtwnre  13182  xrsupsslem  13290  xrinfmsslem  13291  supxrunb1  13302  supxrunb2  13303  ixxdisj  13343  iooshf  13407  icodisj  13457  iccf1o  13477  modid  13865  modadd1  13877  modmul1  13893  seqf1o  14013  expsub  14080  sqlecan  14177  bcval5  14282  hashmap  14399  hashfacen  14417  hashfacenOLD  14418  seqcoll  14429  swrdswrdlem  14658  swrdccatin2  14683  cshwidxmod  14757  2cshwcshw  14780  cshwcshid  14782  resqreu  15203  lenegsq  15271  limsupbnd2  15431  icco1  15488  rlimresb  15513  rlimsqzlem  15599  rlimsqz  15600  rlimsqz2  15601  caucvgrlem  15623  fsum0diag2  15733  o1fsum  15763  ruclem8  16184  dvdsmulcr  16233  ndvdsadd  16357  bitsshft  16420  lcmdvds  16549  hashdvds  16712  eulerthlem2  16719  phisum  16727  pcqmul  16790  pcmpt  16829  prmreclem3  16855  4sqlem11  16892  0ram  16957  ramub1  16965  invfun  17715  initoeu2lem2  17969  coaval  18022  catcisolem  18064  funcestrcsetclem8  18103  fullestrcsetc  18107  embedsetcestrclem  18113  funcsetcestrclem8  18118  fullsetcestrc  18122  prfcl  18159  prf1st  18160  prf2nd  18161  1st2ndprf  18162  curfuncf  18195  isposd  18280  lubun  18472  isacs3lem  18499  pslem  18529  psss  18537  pwsdiagmhm  18748  grpinvid1  18912  grpinvid2  18913  grplcan  18921  grpnpncan0  18955  dfgrp3lem  18957  dfgrp3  18958  grplactcnv  18962  0nsg  19085  eqger  19094  eqg0subg  19111  qus0subgadd  19114  resghm  19146  conjghm  19163  subgga  19205  gaorber  19213  gastacl  19214  orbsta  19218  symgextf1lem  19329  psgnunilem2  19404  odid  19447  odmulg  19465  gexid  19490  odcau  19513  lsmssv  19552  lsmcom2  19564  pj1ghm  19612  frgpuptf  19679  frgpup1  19684  ghmplusg  19755  cyggex2  19806  gsumval3eu  19813  gsumval3  19816  ablfac1eu  19984  pgpfac1lem5  19990  ablsimpgfind  20021  ringurd  20079  isdrngd  20533  isdrngdOLD  20535  issrngd  20612  lmhmf1o  20801  lmhmima  20802  lmhmpreima  20803  lspextmo  20811  pwssplit2  20815  pwssplit3  20816  lspdisj  20883  islbs3  20913  lbsextlem4  20919  drngnidl  21003  rngqiprngghmlem2  21047  rngqiprnglinlem1  21050  rngqiprngghm  21058  lidldvgen  21093  isdomn4  21118  cnsubrg  21205  znunit  21338  cygznlem3  21344  dsmmsubg  21517  dsmmlss  21518  frlmsslsp  21570  frlmup1  21572  lindfrn  21595  f1lindf  21596  issubassa2  21665  psrbagconf1o  21708  psrbagconf1oOLD  21709  psrgrp  21736  evlslem2  21861  mhplss  21917  ply1sclf1  22031  mamuass  22122  dmatmul  22219  dmatsubcl  22220  dmatmulcl  22222  dmatcrng  22224  scmataddcl  22238  scmatsubcl  22239  scmatcrng  22243  mdetunilem2  22335  pm2mpf1  22521  pm2mpghm  22538  eltg2  22681  ntrss  22779  opncldf1  22808  ssnei2  22840  neindisj  22841  restopnb  22899  restntr  22906  tgcmp  23125  hauscmplem  23130  2ndc1stc  23175  2ndcdisj  23180  2ndcomap  23182  restlly  23207  lly1stc  23220  isref  23233  islocfin  23241  comppfsc  23256  txcls  23328  txdis1cn  23359  pthaus  23362  txlm  23372  qtoptop2  23423  qtopomap  23442  kqt0lem  23460  pt1hmeo  23530  ptuncnv  23531  xkocnv  23538  fbasfip  23592  fgabs  23603  fbasrn  23608  elfm2  23672  fmfnfmlem2  23679  fmfnfmlem4  23681  ptcmplem3  23778  ptcmplem4  23779  tsmsres  23868  tsmsxplem1  23877  utoptop  23959  elbl2ps  24115  elbl2  24116  blin  24147  xmeter  24159  xmetresbl  24163  stdbdxmet  24244  metrest  24253  metustexhalf  24285  dscmet  24301  nrmmetd  24303  tngngp2  24389  nmoi2  24467  icccmplem2  24559  reconnlem2  24563  metdstri  24587  metdsle  24588  metdsre  24589  metnrmlem3  24597  fsumcn  24608  icccvx  24690  bndth  24698  evth  24699  reparphti  24737  pi1blem  24779  tcphcph  24978  iscfil2  25007  cfilfcls  25015  iscau4  25020  iscauf  25021  caucfil  25024  cncmet  25063  minveclem7  25176  ovoliunlem1  25243  ovolicc2lem2  25259  ovolicc2lem3  25260  ovolicc2lem4  25261  ovolicc2lem5  25262  ovolicc2  25263  voliunlem3  25293  voliun  25295  ioombl  25306  volivth  25348  ismbfd  25380  ismbf3d  25395  itg1addlem1  25433  i1fadd  25436  itg1addlem4  25440  itg1addlem4OLD  25441  itg2split  25491  itg2monolem1  25492  itg2gt0  25502  ibllem  25506  itgvallem3  25527  iblposlem  25533  bddiblnc  25583  dvmptfsum  25716  rolle  25731  dvlip  25734  c1liplem1  25737  lhop1  25755  lhop2  25756  dvcvx  25761  dvfsumge  25763  dvfsumrlimge0  25771  dvfsumrlim  25772  dvfsum2  25775  mdegaddle  25816  mdegvscale  25817  mdegmullem  25820  ply1divex  25878  coeeulem  25962  plyco  25979  dgrlt  26004  vieta1  26049  ulmss  26133  ulmdvlem3  26138  iblulm  26143  tanord  26271  eff1olem  26281  logdivlt  26353  logccv  26395  lawcos  26545  xrlimcnp  26697  cxp2limlem  26704  cxp2lim  26705  cxploglim2  26707  divsqrtsumo1  26712  lgambdd  26765  sqff1o  26910  dvdsppwf1o  26914  dvdsflf1o  26915  musum  26919  muinv  26921  fsumdvdsmul  26923  sgmmul  26928  fsumvma  26940  logfac2  26944  chpchtsum  26946  logfacrlim  26951  logexprlim  26952  dchrelbas3  26965  dchrmulcl  26976  bposlem1  27011  lgsdchr  27082  lgsquadlem1  27107  lgsquadlem2  27108  lgsquad2lem2  27112  chebbnd1lem1  27196  chpchtlim  27206  rplogsumlem2  27212  dchrmusum2  27221  dchrvmasumlem1  27222  dchrvmasum2lem  27223  dchrvmasumlem2  27225  dchrvmasumlem3  27226  dchrvmasumiflem2  27229  dchrisum0flb  27237  dchrisum0fno1  27238  rpvmasum2  27239  dchrisum0re  27240  dchrisum0lem1  27243  dchrisum0lem2a  27244  dchrisum0lem2  27245  dchrisum0lem3  27246  rplogsum  27254  mulogsum  27259  mulog2sumlem2  27262  vmalogdivsum2  27265  2vmadivsumlem  27267  selberglem2  27273  selberg3lem1  27284  selberg4lem1  27287  selberg4  27288  pntrsumo1  27292  selberg34r  27298  pntrlog2bndlem1  27304  pntrlog2bndlem2  27305  pntrlog2bndlem3  27306  pntrlog2bndlem4  27307  pntrlog2bndlem5  27308  pntrlog2bndlem6  27310  pntibndlem3  27319  pntlemp  27337  ostthlem1  27354  ostth3  27365  sltres  27389  noresle  27424  nosupno  27430  nosupbday  27432  noinfno  27445  bday1s  27557  cutlt  27645  addsproplem2  27680  negsproplem2  27730  mulsuniflem  27831  precsexlem9  27888  precsexlem10  27889  precsexlem11  27890  ercgrg  28023  oppperpex  28259  axlowdimlem15  28469  axlowdimlem16  28470  axcontlem10  28486  cusgrfilem1  28967  upgriswlk  29153  crctcshwlkn0  29330  wwlksnext  29402  wwlksnextwrd  29406  clwlkclwwlklem2a  29506  wwlksext2clwwlk  29565  grpoidinv  30016  grporcan  30026  grpoinvid1  30036  grpoinvid2  30037  grpolcan  30038  ablo4  30058  nvabs  30180  minvecolem7  30391  htthlem  30425  hvadd4  30544  hvaddsub4  30586  shscli  30825  pjspansn  31085  fh1  31126  fh2  31127  cm2j  31128  chscllem2  31146  spansncvi  31160  5oalem2  31163  5oalem5  31166  5oalem6  31167  3oalem2  31171  hoadd4  31292  cnvunop  31426  bralnfn  31456  eighmorth  31472  hmops  31528  hmopm  31529  adjlnop  31594  adjmul  31600  adjadd  31601  nmopcoi  31603  kbass5  31628  kbass6  31629  hstle  31738  stlesi  31749  mdsl0  31818  mdexchi  31843  atom1d  31861  superpos  31862  cvexchlem  31876  atomli  31890  atcvatlem  31893  chirredlem2  31899  chirredlem3  31900  atcvat4i  31905  mdsymlem1  31911  mdsymlem3  31913  mdsymlem5  31915  mdsymlem6  31916  sumdmdlem  31926  sumdmdlem2  31927  cdj1i  31941  opeldifid  32085  isoun  32178  1stpreimas  32182  f1od2  32201  ccatf1  32370  archirngz  32593  archiabllem1  32597  archiabllem2c  32599  qusxpid  32737  indf1ofs  33310  esum2d  33377  cntmeas  33510  ddemeas  33520  carsgclctunlem1  33602  itgeq12dv  33611  eulerpartlemgc  33647  eulerpartlemb  33653  eulerpartlemgs2  33665  ballotlemfc0  33777  ballotlemfcc  33778  reprss  33915  reprpmtf1o  33924  hgt750lemb  33954  bnj607  34213  derangenlem  34448  subfacp1lem3  34459  subfacp1lem5  34461  cvmliftmolem2  34559  cvmliftlem6  34567  cvmlift2lem5  34584  cvmlift2lem7  34586  cvmlift2lem9  34588  mppspstlem  34848  dfon2lem6  35052  colinbtwnle  35382  gg-reparphti  35458  finminlem  35506  nn0prpwlem  35510  isfne  35527  neibastop1  35547  neibastop2lem  35548  neibastop3  35550  tailfb  35565  onsuct0  35629  nndivsub  35645  knoppcnlem6  35677  knoppndvlem9  35699  knoppndvlem18  35708  knoppndvlem21  35711  bj-prmoore  36299  bj-finsumval0  36469  rdgeqoa  36554  pibt2  36601  lindsadd  36784  matunitlindflem2  36788  poimirlem4  36795  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem25  36816  poimirlem28  36819  heicant  36826  mblfinlem2  36829  mblfinlem3  36830  mblfinlem4  36831  mbfposadd  36838  itg2addnclem3  36844  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anc  36872  frinfm  36906  filbcmb  36911  seqpo  36918  sstotbnd2  36945  isbndx  36953  ssbnd  36959  prdsbnd  36964  ismtycnv  36973  ismtyres  36979  heiborlem3  36984  heibor  36992  ghomdiv  37063  grpokerinj  37064  isdrngo2  37129  rngohomco  37145  rngoisocnv  37152  rngoisoco  37153  crngm4  37174  crngohomfo  37177  isidlc  37186  ispridl2  37209  ispridlc  37241  prtlem16  38042  ax12eq  38114  ax12el  38115  lshpcmp  38161  omllaw3  38418  omlfh1N  38431  cvratlem  38595  cvrat3  38616  cvrat4  38617  ps-2  38652  elpaddn0  38974  paddasslem10  39003  cdleme0cp  39388  cdleme32a  39615  cdlemeg49lebilem  39713  cdleme50eq  39715  tendoeq2  39948  diaglbN  40229  diameetN  40230  diainN  40231  dvhopN  40290  djaclN  40310  djajN  40311  dihopelvalcpre  40422  dih1dimatlem  40503  dihmeetcl  40519  djhcl  40574  mapdpglem2  40847  3factsumint1  41192  sticksstones22  41290  metakunt2  41292  imacrhmcl  41393  frlmsnic  41412  evlselvlem  41460  fsuppind  41464  0prjspn  41672  infdesc  41687  ismrc  41741  eldioph2  41802  lzenom  41810  rexrabdioph  41834  fphpdo  41857  irrapxlem3  41864  elpell14qr2  41902  pell14qrreccl  41904  pell14qrdich  41909  pellfundglb  41925  monotoddzzfi  41983  2nn0ind  41986  jm2.21  42035  jm2.22  42036  dnnumch3  42091  dnwech  42092  fnwe2lem2  42095  hbtlem6  42173  cantnfresb  42376  imo72b2lem1  43223  mnuprdlem1  43333  mnuprdlem2  43334  cncmpmax  44018  disjf1  44181  eliccelioc  44533  fprodexp  44609  fprodabs2  44610  mullimc  44631  mullimcf  44638  islpcn  44654  limsuppnfdlem  44716  liminfval2  44783  xlimmnfvlem1  44847  xlimmnfvlem2  44848  xlimpnfvlem1  44851  xlimpnfvlem2  44852  cncfshift  44889  cncfperiod  44894  fprodcncf  44915  dvnprodlem1  44961  dvnprodlem2  44962  stoweidlem34  45049  stoweidlem48  45063  stoweidlem60  45075  fourierdlem42  45164  fourierdlem60  45181  fourierdlem61  45182  fourierdlem63  45184  fourierdlem65  45186  fourierdlem87  45208  fourierdlem97  45218  elaa2  45249  etransclem46  45295  etransc  45298  salrestss  45376  sge0iunmptlemfi  45428  isomennd  45546  ovnsslelem  45575  ovolval4lem2  45665  smflimlem3  45788  smflimlem4  45789  smflimlem6  45791  smfpimbor1lem1  45813  smflimmpt  45825  smflimsupmpt  45844  smfliminfmpt  45847  fsetsnf1  46061  fcoresf1  46078  fvelsetpreimafv  46354  icceuelpart  46403  prproropf1olem4  46473  fmtnoprmfac2  46534  bgoldbtbndlem2  46773  bgoldbtbndlem3  46774  srhmsubc  47063  srhmsubcALTV  47081  catprs  47719  prsthinc  47762  aacllem  47936