Theorem adantrr 730

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antrl  741  ad2ant2r  760  ad2ant2lr  761  cases2ALT  1064  consensus  1068  3adant3  1150  3ad2antr1  1207  reusv2lem3  5373  axprlem4OLD  5403  otsndisj  5504  otiunsndisj  5505  po2nr  5585  sotric  5601  sotrieq  5602  tz7.7  6390  fmptsnd  7171  fvtp1g  7200  f1cofveqaeqALT  7258  fsnex  7287  isocnv  7334  isores2  7337  isomin  7341  isoini  7342  f1oiso2  7356  ovmpodf  7572  offval  7689  ordsucun  7823  xp1st  8020  cnvf1olem  8107  fnse  8131  sexp2  8144  mpoxopoveq  8217  frrlem3  8287  frrlem13  8297  oalim  8519  omlim  8520  oaass  8548  omordi  8553  omwordri  8559  odi  8566  oen0  8574  oewordri  8580  nnawordi  8609  nnmordi  8619  omabs  8639  coflton  8659  nadd4  8687  erinxp  8791  dom2lem  8991  domssl  8997  mapen  9132  ssenen  9142  ssfiALT  9161  domfi  9176  php  9194  domunfican  9284  mapfien  9371  ordtypelem6  9488  ordtypelem7  9489  card2inf  9520  inf3lem6  9605  cantnfle  9643  cantnflem1b  9658  cantnflem1  9661  wemapwe  9669  ttrclselem2  9698  rankxplim3  9856  fseqenlem2  10021  dfac5lem4  10122  dfac2b  10126  cfsuc  10252  cfflb  10254  cofsmo  10264  infpssrlem4  10301  fin4en1  10304  ssfin4  10305  fin23lem26  10320  fin23lem22  10322  fin23lem27  10323  isf34lem4  10372  isf34lem5  10373  fin1a2lem12  10406  axdc3lem2  10446  axdc4lem  10450  ttukeylem6  10509  iundom2g  10535  pwcfsdom  10579  gchen2  10622  gchor  10623  fpwwe2lem6  10632  fpwwe2lem8  10634  fpwwe2lem10  10636  fpwwe2lem11  10637  fpwwe2  10639  pwfseqlem4  10658  gchina  10695  ltexprlem6  11037  prlem936  11043  mul4  11389  2addsub  11482  muladd  11657  ltleadd  11708  leord1  11752  eqord1  11753  ltord2  11754  leord2  11755  eqord2  11756  divmul3  11888  divcan7  11935  divadddiv  11941  lemul2a  12081  lemul12b  12083  ltmuldiv2  12100  ltdivmul  12101  ledivmul  12102  ltdivmul2  12103  lt2mul2div  12104  ledivmul2  12105  lemuldiv2  12107  lt2msq  12111  ltdiv23  12117  lediv23  12118  fimaxre  12170  supadd  12194  supmullem1  12196  cju  12225  zextlt  12681  suprzcl  12687  zmax  12980  xrlttr  13176  xrre3  13208  qbtwnre  13236  xrsupsslem  13344  xrinfmsslem  13345  supxrunb1  13356  supxrunb2  13357  ixxdisj  13398  iooshf  13464  icodisj  13514  iccf1o  13534  modid  13942  modadd1  13954  modmul1  13973  seqf1o  14092  expsub  14159  sqlecan  14258  bcval5  14367  hashmap  14485  hashfacen  14504  seqcoll  14514  ccatf1  14641  swrdswrdlem  14758  swrdccatin2  14783  cshwidxmod  14859  2cshwcshw  14881  cshwcshid  14883  resqreu  15322  lenegsq  15391  limsupbnd2  15553  icco1  15610  rlimresb  15635  rlimsqzlem  15719  rlimsqz  15720  rlimsqz2  15721  caucvgrlem  15743  fsum0diag2  15852  o1fsum  15883  ruclem8  16310  dvdsmulcr  16360  ndvdsadd  16485  bitsshft  16550  lcmdvds  16683  hashdvds  16851  eulerthlem2  16858  phisum  16867  pcqmul  16930  pcmpt  16969  prmreclem3  16995  4sqlem11  17032  0ram  17097  ramub1  17105  invfun  17838  initoeu2lem2  18089  coaval  18142  catcisolem  18184  funcestrcsetclem8  18220  fullestrcsetc  18224  embedsetcestrclem  18230  funcsetcestrclem8  18235  fullsetcestrc  18239  prfcl  18276  prf1st  18277  prf2nd  18278  1st2ndprf  18279  curfuncf  18311  isposd  18395  lubun  18588  isacs3lem  18615  pslem  18645  psss  18653  chnccat  18699  chnpof1  18703  pwsdiagmhm  18913  grpinvid1  19081  grpinvid2  19082  grplcan  19090  grpnpncan0  19125  dfgrp3lem  19127  dfgrp3  19128  grplactcnv  19132  0nsg  19258  eqger  19269  qusxpid  19274  eqg0subg  19290  qus0subgadd  19293  resghm  19325  conjghm  19342  subgga  19393  gaorber  19401  gastacl  19402  orbsta  19406  symgextf1lem  19513  psgnunilem2  19588  odid  19631  odmulg  19649  gexid  19674  odcau  19697  lsmssv  19736  lsmcom2  19748  pj1ghm  19796  frgpuptf  19863  frgpup1  19868  ghmplusg  19939  cyggex2  19990  gsumval3eu  19997  gsumval3  20000  ablfac1eu  20168  pgpfac1lem5  20174  ablsimpgfind  20205  ringurd  20290  srhmsubc  20808  isdomn4  20843  isdrngd  20897  isdrngdOLD  20899  issrngd  20987  lmhmf1o  21196  lmhmima  21197  lmhmpreima  21198  lspextmo  21206  pwssplit2  21210  pwssplit3  21211  lspdisj  21278  islbs3  21308  lbsextlem4  21314  drngnidl  21406  rngqiprngghmlem2  21457  rngqiprnglinlem1  21460  rngqiprngghm  21468  lidldvgen  21531  cnsubrg  21606  znunit  21742  cygznlem3  21748  dsmmsubg  21922  dsmmlss  21923  frlmsslsp  21975  frlmup1  21977  lindfrn  22000  f1lindf  22001  issubassa2  22071  psrbagconf1o  22108  psrgrp  22135  evlslem2  22259  mhplss  22347  psdmul  22358  psdmvr  22361  ply1sclf1  22479  mamuass  22588  dmatmul  22683  dmatsubcl  22684  dmatmulcl  22686  dmatcrng  22688  scmataddcl  22702  scmatsubcl  22703  scmatcrng  22707  mdetunilem2  22799  pm2mpf1  22985  pm2mpghm  23002  eltg2  23144  ntrss  23241  opncldf1  23270  ssnei2  23302  neindisj  23303  restopnb  23361  restntr  23368  tgcmp  23587  hauscmplem  23592  2ndc1stc  23637  2ndcdisj  23642  2ndcomap  23644  restlly  23669  lly1stc  23682  isref  23695  islocfin  23703  comppfsc  23718  txcls  23790  txdis1cn  23821  pthaus  23824  txlm  23834  qtoptop2  23885  qtopomap  23904  kqt0lem  23922  pt1hmeo  23992  ptuncnv  23993  xkocnv  24000  fbasfip  24054  fgabs  24065  fbasrn  24070  elfm2  24134  fmfnfmlem2  24141  fmfnfmlem4  24143  ptcmplem3  24240  ptcmplem4  24241  tsmsres  24330  tsmsxplem1  24339  utoptop  24420  elbl2ps  24575  elbl2  24576  blin  24607  xmeter  24619  xmetresbl  24623  stdbdxmet  24701  metrest  24710  metustexhalf  24742  dscmet  24758  nrmmetd  24760  tngngp2  24838  nmoi2  24916  icccmplem2  25010  reconnlem2  25014  metdstri  25038  metdsle  25039  metdsre  25040  metnrmlem3  25048  fsumcn  25058  icccvx  25138  bndth  25146  evth  25147  reparphti  25185  pi1blem  25227  tcphcph  25425  iscfil2  25454  cfilfcls  25462  iscau4  25467  iscauf  25468  caucfil  25471  cncmet  25510  minveclem7  25623  ovoliunlem1  25690  ovolicc2lem2  25706  ovolicc2lem3  25707  ovolicc2lem4  25708  ovolicc2lem5  25709  ovolicc2  25710  voliunlem3  25740  voliun  25742  ioombl  25753  volivth  25795  ismbfd  25827  ismbf3d  25842  itg1addlem1  25880  i1fadd  25883  itg1addlem4  25887  itg2split  25937  itg2monolem1  25938  itg2gt0  25948  ibllem  25952  itgvallem3  25974  iblposlem  25980  bddiblnc  26030  dvmptfsum  26163  rolle  26178  dvlip  26181  c1liplem1  26184  lhop1  26202  lhop2  26203  dvcvx  26208  dvfsumge  26210  dvfsumrlimge0  26218  dvfsumrlim  26219  dvfsum2  26222  mdegaddle  26260  mdegvscale  26261  mdegmullem  26264  ply1divex  26323  coeeulem  26410  plyco  26427  dgrlt  26452  vieta1  26502  ulmss  26589  ulmdvlem3  26594  iblulm  26599  tanord  26732  eff1olem  26742  logdivlt  26815  logccv  26857  lawcos  27010  xrlimcnp  27162  cxp2limlem  27169  cxp2lim  27170  cxploglim2  27172  divsqrtsumo1  27177  lgambdd  27230  sqff1o  27375  dvdsppwf1o  27379  dvdsflf1o  27380  musum  27384  muinv  27386  fsumdvdsmul  27388  sgmmul  27394  fsumvma  27406  logfac2  27410  chpchtsum  27412  logfacrlim  27417  logexprlim  27418  dchrelbas3  27431  dchrmulcl  27442  bposlem1  27477  lgsdchr  27548  lgsquadlem1  27573  lgsquadlem2  27574  lgsquad2lem2  27578  chebbnd1lem1  27662  chpchtlim  27672  rplogsumlem2  27678  dchrmusum2  27687  dchrvmasumlem1  27688  dchrvmasum2lem  27689  dchrvmasumlem2  27691  dchrvmasumlem3  27692  dchrvmasumiflem2  27695  dchrisum0flb  27703  dchrisum0fno1  27704  rpvmasum2  27705  dchrisum0re  27706  dchrisum0lem1  27709  dchrisum0lem2a  27710  dchrisum0lem2  27711  dchrisum0lem3  27712  rplogsum  27720  mulogsum  27725  mulog2sumlem2  27728  vmalogdivsum2  27731  2vmadivsumlem  27733  selberglem2  27739  selberg3lem1  27750  selberg4lem1  27753  selberg4  27754  pntrsumo1  27758  selberg34r  27764  pntrlog2bndlem1  27770  pntrlog2bndlem2  27771  pntrlog2bndlem3  27772  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  pntrlog2bndlem6  27776  pntibndlem3  27785  pntlemp  27803  ostthlem1  27820  ostth3  27831  ltsres  27855  noresle  27890  nosupno  27896  nosupbday  27898  noinfno  27911  bday1  28036  cutlt  28154  addsproplem2  28192  negsproplem2  28251  mulsuniflem  28371  mulsunif2lem  28391  precsexlem9  28437  precsexlem10  28438  precsexlem11  28439  om2noseqlt  28521  om2noseqlt2  28522  om2noseqf1o  28523  om2noseqrdg  28526  noseqrdgfn  28528  bdaypw2n0bndlem  28685  bdayfinbndlem1  28689  recut  28716  elreno2  28717  renegscl  28720  ercgrg  28815  oppperpex  29063  axlowdimlem15  29335  axlowdimlem16  29336  axcontlem10  29352  cusgrfilem1  29834  upgriswlk  30019  crctcshwlkn0  30199  wwlksnext  30271  wwlksnextwrd  30275  clwlkclwwlklem2a  30378  wwlksext2clwwlk  30437  grpoidinv  30889  grporcan  30899  grpoinvid1  30909  grpoinvid2  30910  grpolcan  30911  ablo4  30931  nvabs  31053  minvecolem7  31264  htthlem  31298  hvadd4  31417  hvaddsub4  31459  shscli  31698  pjspansn  31958  fh1  31999  fh2  32000  cm2j  32001  chscllem2  32019  spansncvi  32033  5oalem2  32036  5oalem5  32039  5oalem6  32040  3oalem2  32044  hoadd4  32165  cnvunop  32299  bralnfn  32329  eighmorth  32345  hmops  32401  hmopm  32402  adjlnop  32467  adjmul  32473  adjadd  32474  nmopcoi  32476  kbass5  32501  kbass6  32502  hstle  32611  stlesi  32622  mdsl0  32691  mdexchi  32716  atom1d  32734  superpos  32735  cvexchlem  32749  atomli  32763  atcvatlem  32766  chirredlem2  32772  chirredlem3  32773  atcvat4i  32778  mdsymlem1  32784  mdsymlem3  32786  mdsymlem5  32788  mdsymlem6  32789  sumdmdlem  32799  sumdmdlem2  32800  cdj1i  32814  opeldifid  32973  isoun  33076  1stpreimas  33080  f1od2  33093  indf1ofs  33215  archirngz  33532  archiabllem1  33536  archiabllem2c  33538  esum2d  34506  cntmeas  34640  ddemeas  34650  carsgclctunlem1  34731  itgeq12dv  34740  eulerpartlemgc  34776  eulerpartlemb  34782  eulerpartlemgs2  34794  ballotlemfc0  34907  ballotlemfcc  34908  reprss  35028  reprpmtf1o  35037  hgt750lemb  35067  bnj607  35328  fissorduni  35497  derangenlem  35676  subfacp1lem3  35687  subfacp1lem5  35689  cvmliftmolem2  35787  cvmliftlem6  35795  cvmlift2lem5  35812  cvmlift2lem7  35814  cvmlift2lem9  35816  mppspstlem  36076  dfon2lem6  36291  colinbtwnle  36623  nmulrid  36702  ltnadd  36723  nadddilem2  36726  nadddilem4  36728  finminlem  36862  nn0prpwlem  36866  isfne  36883  neibastop1  36903  neibastop2lem  36904  neibastop3  36906  tailfb  36921  onsuct0  36985  nndivsub  37001  mh-inf3f1  37085  knoppcnlem6  37120  knoppndvlem9  37142  knoppndvlem18  37151  knoppndvlem21  37154  bj-prmoore  37790  bj-finsumval0  37962  rdgeqoa  38049  pibt2  38096  lindsadd  38297  matunitlindflem2  38301  poimirlem4  38308  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem25  38329  poimirlem28  38332  heicant  38339  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  mbfposadd  38351  itg2addnclem3  38357  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anc  38385  frinfm  38419  filbcmb  38424  seqpo  38431  sstotbnd2  38458  isbndx  38466  ssbnd  38472  prdsbnd  38477  ismtycnv  38486  ismtyres  38492  heiborlem3  38497  heibor  38505  ghomdiv  38576  grpokerinj  38577  isdrngo2  38642  rngohomco  38658  rngoisocnv  38665  rngoisoco  38666  crngm4  38687  crngohomfo  38690  isidlc  38699  ispridl2  38722  ispridlc  38754  prtlem16  39676  ax12eq  39748  ax12el  39749  lshpcmp  39795  omllaw3  40052  omlfh1N  40065  cvratlem  40228  cvrat3  40249  cvrat4  40250  ps-2  40285  elpaddn0  40607  paddasslem10  40636  cdleme0cp  41021  cdleme32a  41248  cdlemeg49lebilem  41346  cdleme50eq  41348  tendoeq2  41581  diaglbN  41862  diameetN  41863  diainN  41864  dvhopN  41923  djaclN  41943  djajN  41944  dihopelvalcpre  42055  dih1dimatlem  42136  dihmeetcl  42152  djhcl  42207  mapdpglem2  42480  3factsumint1  42821  sticksstones22  42968  unitscyglem4  42998  imacrhmcl  43321  frlmsnic  43341  psrmnd  43344  evlselvlem  43353  fsuppind  43355  0prjspn  43393  infdesc  43408  ismrc  43465  eldioph2  43526  lzenom  43534  rexrabdioph  43554  fphpdo  43577  irrapxlem3  43584  elpell14qr2  43622  pell14qrreccl  43624  pell14qrdich  43629  pellfundglb  43645  monotoddzzfi  43702  2nn0ind  43705  jm2.21  43754  jm2.22  43755  dnnumch3  43807  dnwech  43808  fnwe2lem2  43811  hbtlem6  43889  cantnfresb  44084  imo72b2lem1  44928  mnuprdlem1  45015  mnuprdlem2  45016  relpmin  45694  traxext  45719  cncmpmax  45785  disjf1  45934  eliccelioc  46270  fprodexp  46343  fprodabs2  46344  mullimc  46365  mullimcf  46372  islpcn  46386  limsuppnfdlem  46448  liminfval2  46515  xlimmnfvlem1  46579  xlimmnfvlem2  46580  xlimpnfvlem1  46583  xlimpnfvlem2  46584  cncfshift  46621  cncfperiod  46626  fprodcncf  46647  dvnprodlem1  46693  dvnprodlem2  46694  stoweidlem34  46781  stoweidlem48  46795  stoweidlem60  46807  fourierdlem42  46896  fourierdlem60  46913  fourierdlem61  46914  fourierdlem63  46916  fourierdlem65  46918  fourierdlem87  46940  fourierdlem97  46950  elaa2  46981  etransclem46  47027  etransc  47030  salrestss  47108  sge0iunmptlemfi  47160  isomennd  47278  ovnsslelem  47307  ovolval4lem2  47397  smflimlem3  47520  smflimlem4  47521  smflimlem6  47523  smfpimbor1lem1  47545  smflimmpt  47557  smflimsupmpt  47576  smfliminfmpt  47579  fsetsnf1  47822  fcoresf1  47839  fvelsetpreimafv  48169  icceuelpart  48218  prproropf1olem4  48288  fmtnoprmfac2  48352  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  gpg3nbgrvtx0ALT  48875  gpg3nbgrvtx1  48876  srhmsubcALTV  49123  xpco2  49668  catprs  49822  uppropd  49992  thincciso2  50266  prsthinc  50275  functermc  50319  fulltermc  50322  lmdran  50482  cmdlan  50483  aacllem  50654