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  5342  axprlem4OLD  5371  otsndisj  5466  otiunsndisj  5467  po2nr  5545  sotric  5561  sotrieq  5562  tz7.7  6337  fmptsnd  7109  fvtp1g  7138  f1cofveqaeqALT  7199  fsnex  7224  isocnv  7271  isores2  7274  isomin  7278  isoini  7279  f1oiso2  7293  ovmpodf  7509  offval  7626  ordsucun  7764  xp1st  7963  cnvf1olem  8050  fnse  8073  sexp2  8086  mpoxopoveq  8159  frrlem3  8228  frrlem13  8238  oalim  8457  omlim  8458  oaass  8486  omordi  8491  omwordri  8497  odi  8504  oen0  8511  oewordri  8517  nnawordi  8546  nnmordi  8556  omabs  8576  coflton  8596  nadd4  8623  erinxp  8725  dom2lem  8924  domssl  8930  mapen  9065  ssenen  9075  ssfiALT  9098  domfi  9113  php  9131  domunfican  9230  mapfien  9317  ordtypelem6  9434  ordtypelem7  9435  card2inf  9466  inf3lem6  9548  cantnfle  9586  cantnflem1b  9601  cantnflem1  9604  wemapwe  9612  ttrclselem2  9641  rankxplim3  9796  fseqenlem2  9938  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  cfsuc  10170  cfflb  10172  cofsmo  10182  infpssrlem4  10219  fin4en1  10222  ssfin4  10223  fin23lem26  10238  fin23lem22  10240  fin23lem27  10241  isf34lem4  10290  isf34lem5  10291  fin1a2lem12  10324  axdc3lem2  10364  axdc4lem  10368  ttukeylem6  10427  iundom2g  10453  pwcfsdom  10496  gchen2  10539  gchor  10540  fpwwe2lem6  10549  fpwwe2lem8  10551  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2  10556  pwfseqlem4  10575  gchina  10612  ltexprlem6  10954  prlem936  10960  mul4  11302  2addsub  11395  muladd  11570  ltleadd  11621  leord1  11665  eqord1  11666  ltord2  11667  leord2  11668  eqord2  11669  divmul3  11802  divcan7  11851  divadddiv  11857  lemul2a  11997  lemul12b  11999  ltmuldiv2  12017  ltdivmul  12018  ledivmul  12019  ltdivmul2  12020  lt2mul2div  12021  ledivmul2  12022  lemuldiv2  12024  lt2msq  12028  ltdiv23  12034  lediv23  12035  fimaxre  12087  supadd  12111  supmullem1  12113  cju  12142  zextlt  12568  suprzcl  12574  zmax  12864  xrlttr  13060  xrre3  13091  qbtwnre  13119  xrsupsslem  13227  xrinfmsslem  13228  supxrunb1  13239  supxrunb2  13240  ixxdisj  13281  iooshf  13347  icodisj  13397  iccf1o  13417  modid  13818  modadd1  13830  modmul1  13849  seqf1o  13968  expsub  14035  sqlecan  14134  bcval5  14243  hashmap  14360  hashfacen  14379  seqcoll  14389  swrdswrdlem  14628  swrdccatin2  14653  cshwidxmod  14727  2cshwcshw  14750  cshwcshid  14752  resqreu  15177  lenegsq  15246  limsupbnd2  15408  icco1  15465  rlimresb  15490  rlimsqzlem  15574  rlimsqz  15575  rlimsqz2  15576  caucvgrlem  15598  fsum0diag2  15708  o1fsum  15738  ruclem8  16164  dvdsmulcr  16214  ndvdsadd  16339  bitsshft  16404  lcmdvds  16537  hashdvds  16704  eulerthlem2  16711  phisum  16720  pcqmul  16783  pcmpt  16822  prmreclem3  16848  4sqlem11  16885  0ram  16950  ramub1  16958  invfun  17689  initoeu2lem2  17940  coaval  17993  catcisolem  18035  funcestrcsetclem8  18071  fullestrcsetc  18075  embedsetcestrclem  18081  funcsetcestrclem8  18086  fullsetcestrc  18090  prfcl  18127  prf1st  18128  prf2nd  18129  1st2ndprf  18130  curfuncf  18162  isposd  18246  lubun  18439  isacs3lem  18466  pslem  18496  psss  18504  pwsdiagmhm  18723  grpinvid1  18888  grpinvid2  18889  grplcan  18897  grpnpncan0  18933  dfgrp3lem  18935  dfgrp3  18936  grplactcnv  18940  0nsg  19066  eqger  19075  eqg0subg  19093  qus0subgadd  19096  resghm  19129  conjghm  19146  subgga  19197  gaorber  19205  gastacl  19206  orbsta  19210  symgextf1lem  19317  psgnunilem2  19392  odid  19435  odmulg  19453  gexid  19478  odcau  19501  lsmssv  19540  lsmcom2  19552  pj1ghm  19600  frgpuptf  19667  frgpup1  19672  ghmplusg  19743  cyggex2  19794  gsumval3eu  19801  gsumval3  19804  ablfac1eu  19972  pgpfac1lem5  19978  ablsimpgfind  20009  ringurd  20088  srhmsubc  20583  isdomn4  20619  isdrngd  20668  isdrngdOLD  20670  issrngd  20758  lmhmf1o  20968  lmhmima  20969  lmhmpreima  20970  lspextmo  20978  pwssplit2  20982  pwssplit3  20983  lspdisj  21050  islbs3  21080  lbsextlem4  21086  drngnidl  21168  rngqiprngghmlem2  21213  rngqiprnglinlem1  21216  rngqiprngghm  21224  lidldvgen  21259  cnsubrg  21352  znunit  21488  cygznlem3  21494  dsmmsubg  21668  dsmmlss  21669  frlmsslsp  21721  frlmup1  21723  lindfrn  21746  f1lindf  21747  issubassa2  21817  psrbagconf1o  21854  psrgrp  21881  evlslem2  22002  mhplss  22058  psdmul  22069  psdmvr  22072  ply1sclf1  22191  mamuass  22305  dmatmul  22400  dmatsubcl  22401  dmatmulcl  22403  dmatcrng  22405  scmataddcl  22419  scmatsubcl  22420  scmatcrng  22424  mdetunilem2  22516  pm2mpf1  22702  pm2mpghm  22719  eltg2  22861  ntrss  22958  opncldf1  22987  ssnei2  23019  neindisj  23020  restopnb  23078  restntr  23085  tgcmp  23304  hauscmplem  23309  2ndc1stc  23354  2ndcdisj  23359  2ndcomap  23361  restlly  23386  lly1stc  23399  isref  23412  islocfin  23420  comppfsc  23435  txcls  23507  txdis1cn  23538  pthaus  23541  txlm  23551  qtoptop2  23602  qtopomap  23621  kqt0lem  23639  pt1hmeo  23709  ptuncnv  23710  xkocnv  23717  fbasfip  23771  fgabs  23782  fbasrn  23787  elfm2  23851  fmfnfmlem2  23858  fmfnfmlem4  23860  ptcmplem3  23957  ptcmplem4  23958  tsmsres  24047  tsmsxplem1  24056  utoptop  24138  elbl2ps  24293  elbl2  24294  blin  24325  xmeter  24337  xmetresbl  24341  stdbdxmet  24419  metrest  24428  metustexhalf  24460  dscmet  24476  nrmmetd  24478  tngngp2  24556  nmoi2  24634  icccmplem2  24728  reconnlem2  24732  metdstri  24756  metdsle  24757  metdsre  24758  metnrmlem3  24766  fsumcn  24777  icccvx  24864  bndth  24873  evth  24874  reparphti  24912  reparphtiOLD  24913  pi1blem  24955  tcphcph  25153  iscfil2  25182  cfilfcls  25190  iscau4  25195  iscauf  25196  caucfil  25199  cncmet  25238  minveclem7  25351  ovoliunlem1  25419  ovolicc2lem2  25435  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2lem5  25438  ovolicc2  25439  voliunlem3  25469  voliun  25471  ioombl  25482  volivth  25524  ismbfd  25556  ismbf3d  25571  itg1addlem1  25609  i1fadd  25612  itg1addlem4  25616  itg2split  25666  itg2monolem1  25667  itg2gt0  25677  ibllem  25681  itgvallem3  25703  iblposlem  25709  bddiblnc  25759  dvmptfsum  25895  rolle  25910  dvlip  25914  c1liplem1  25917  lhop1  25935  lhop2  25936  dvcvx  25941  dvfsumge  25944  dvfsumrlimge0  25953  dvfsumrlim  25954  dvfsum2  25957  mdegaddle  25995  mdegvscale  25996  mdegmullem  25999  ply1divex  26058  coeeulem  26145  plyco  26162  dgrlt  26188  vieta1  26236  ulmss  26322  ulmdvlem3  26327  iblulm  26332  tanord  26463  eff1olem  26473  logdivlt  26546  logccv  26588  lawcos  26742  xrlimcnp  26894  cxp2limlem  26902  cxp2lim  26903  cxploglim2  26905  divsqrtsumo1  26910  lgambdd  26963  sqff1o  27108  dvdsppwf1o  27112  dvdsflf1o  27113  musum  27117  muinv  27119  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  sgmmul  27128  fsumvma  27140  logfac2  27144  chpchtsum  27146  logfacrlim  27151  logexprlim  27152  dchrelbas3  27165  dchrmulcl  27176  bposlem1  27211  lgsdchr  27282  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2lem2  27312  chebbnd1lem1  27396  chpchtlim  27406  rplogsumlem2  27412  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem2  27429  dchrisum0flb  27437  dchrisum0fno1  27438  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  rplogsum  27454  mulogsum  27459  mulog2sumlem2  27462  vmalogdivsum2  27465  2vmadivsumlem  27467  selberglem2  27473  selberg3lem1  27484  selberg4lem1  27487  selberg4  27488  pntrsumo1  27492  selberg34r  27498  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntibndlem3  27519  pntlemp  27537  ostthlem1  27554  ostth3  27565  sltres  27590  noresle  27625  nosupno  27631  nosupbday  27633  noinfno  27646  bday1s  27763  cutlt  27863  addsproplem2  27900  negsproplem2  27958  mulsuniflem  28075  mulsunif2lem  28095  precsexlem9  28140  precsexlem10  28141  precsexlem11  28142  om2noseqlt  28216  om2noseqlt2  28217  om2noseqf1o  28218  om2noseqrdg  28221  noseqrdgfn  28223  recut  28383  renegscl  28385  ercgrg  28480  oppperpex  28716  axlowdimlem15  28919  axlowdimlem16  28920  axcontlem10  28936  cusgrfilem1  29419  upgriswlk  29604  crctcshwlkn0  29784  wwlksnext  29856  wwlksnextwrd  29860  clwlkclwwlklem2a  29960  wwlksext2clwwlk  30019  grpoidinv  30470  grporcan  30480  grpoinvid1  30490  grpoinvid2  30491  grpolcan  30492  ablo4  30512  nvabs  30634  minvecolem7  30845  htthlem  30879  hvadd4  30998  hvaddsub4  31040  shscli  31279  pjspansn  31539  fh1  31580  fh2  31581  cm2j  31582  chscllem2  31600  spansncvi  31614  5oalem2  31617  5oalem5  31620  5oalem6  31621  3oalem2  31625  hoadd4  31746  cnvunop  31880  bralnfn  31910  eighmorth  31926  hmops  31982  hmopm  31983  adjlnop  32048  adjmul  32054  adjadd  32055  nmopcoi  32057  kbass5  32082  kbass6  32083  hstle  32192  stlesi  32203  mdsl0  32272  mdexchi  32297  atom1d  32315  superpos  32316  cvexchlem  32330  atomli  32344  atcvatlem  32347  chirredlem2  32353  chirredlem3  32354  atcvat4i  32359  mdsymlem1  32365  mdsymlem3  32367  mdsymlem5  32369  mdsymlem6  32370  sumdmdlem  32380  sumdmdlem2  32381  cdj1i  32395  opeldifid  32561  isoun  32658  1stpreimas  32662  f1od2  32677  indf1ofs  32822  ccatf1  32903  archirngz  33141  archiabllem1  33145  archiabllem2c  33147  qusxpid  33310  esum2d  34059  cntmeas  34192  ddemeas  34202  carsgclctunlem1  34284  itgeq12dv  34293  eulerpartlemgc  34329  eulerpartlemb  34335  eulerpartlemgs2  34347  ballotlemfc0  34460  ballotlemfcc  34461  reprss  34584  reprpmtf1o  34593  hgt750lemb  34623  bnj607  34882  derangenlem  35143  subfacp1lem3  35154  subfacp1lem5  35156  cvmliftmolem2  35254  cvmliftlem6  35262  cvmlift2lem5  35279  cvmlift2lem7  35281  cvmlift2lem9  35283  mppspstlem  35543  dfon2lem6  35761  colinbtwnle  36091  finminlem  36291  nn0prpwlem  36295  isfne  36312  neibastop1  36332  neibastop2lem  36333  neibastop3  36335  tailfb  36350  onsuct0  36414  nndivsub  36430  knoppcnlem6  36471  knoppndvlem9  36493  knoppndvlem18  36502  knoppndvlem21  36505  bj-prmoore  37088  bj-finsumval0  37258  rdgeqoa  37343  pibt2  37390  lindsadd  37592  matunitlindflem2  37596  poimirlem4  37603  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem25  37624  poimirlem28  37627  heicant  37634  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  mbfposadd  37646  itg2addnclem3  37652  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anc  37680  frinfm  37714  filbcmb  37719  seqpo  37726  sstotbnd2  37753  isbndx  37761  ssbnd  37767  prdsbnd  37772  ismtycnv  37781  ismtyres  37787  heiborlem3  37792  heibor  37800  ghomdiv  37871  grpokerinj  37872  isdrngo2  37937  rngohomco  37953  rngoisocnv  37960  rngoisoco  37961  crngm4  37982  crngohomfo  37985  isidlc  37994  ispridl2  38017  ispridlc  38049  prtlem16  38847  ax12eq  38919  ax12el  38920  lshpcmp  38966  omllaw3  39223  omlfh1N  39236  cvratlem  39400  cvrat3  39421  cvrat4  39422  ps-2  39457  elpaddn0  39779  paddasslem10  39808  cdleme0cp  40193  cdleme32a  40420  cdlemeg49lebilem  40518  cdleme50eq  40520  tendoeq2  40753  diaglbN  41034  diameetN  41035  diainN  41036  dvhopN  41095  djaclN  41115  djajN  41116  dihopelvalcpre  41227  dih1dimatlem  41308  dihmeetcl  41324  djhcl  41379  mapdpglem2  41652  3factsumint1  41994  sticksstones22  42141  unitscyglem4  42171  imacrhmcl  42487  frlmsnic  42513  psrmnd  42518  evlselvlem  42559  fsuppind  42563  0prjspn  42601  infdesc  42616  ismrc  42674  eldioph2  42735  lzenom  42743  rexrabdioph  42767  fphpdo  42790  irrapxlem3  42797  elpell14qr2  42835  pell14qrreccl  42837  pell14qrdich  42842  pellfundglb  42858  monotoddzzfi  42915  2nn0ind  42918  jm2.21  42967  jm2.22  42968  dnnumch3  43020  dnwech  43021  fnwe2lem2  43024  hbtlem6  43102  cantnfresb  43297  imo72b2lem1  44142  mnuprdlem1  44245  mnuprdlem2  44246  relpmin  44926  traxext  44951  cncmpmax  45010  disjf1  45161  eliccelioc  45503  fprodexp  45576  fprodabs2  45577  mullimc  45598  mullimcf  45605  islpcn  45621  limsuppnfdlem  45683  liminfval2  45750  xlimmnfvlem1  45814  xlimmnfvlem2  45815  xlimpnfvlem1  45818  xlimpnfvlem2  45819  cncfshift  45856  cncfperiod  45861  fprodcncf  45882  dvnprodlem1  45928  dvnprodlem2  45929  stoweidlem34  46016  stoweidlem48  46030  stoweidlem60  46042  fourierdlem42  46131  fourierdlem60  46148  fourierdlem61  46149  fourierdlem63  46151  fourierdlem65  46153  fourierdlem87  46175  fourierdlem97  46185  elaa2  46216  etransclem46  46262  etransc  46265  salrestss  46343  sge0iunmptlemfi  46395  isomennd  46513  ovnsslelem  46542  ovolval4lem2  46632  smflimlem3  46755  smflimlem4  46756  smflimlem6  46758  smfpimbor1lem1  46780  smflimmpt  46792  smflimsupmpt  46811  smfliminfmpt  46814  fsetsnf1  47037  fcoresf1  47054  fvelsetpreimafv  47372  icceuelpart  47421  prproropf1olem4  47491  fmtnoprmfac2  47552  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  gpgnbgrvtx0  48059  gpgnbgrvtx1  48060  gpg3nbgrvtx0ALT  48062  gpg3nbgrvtx1  48063  srhmsubcALTV  48310  xpco2  48842  catprs  48997  uppropd  49167  thincciso2  49441  prsthinc  49450  functermc  49494  fulltermc  49497  lmdran  49657  cmdlan  49658  aacllem  49787