Theorem adantrr 704

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  ad2ant2r  734  ad2ant2lr  735  cases2ALT  1029  consensus  1033  3adant3  1112  3ad2antr1  1168  reusv2lem3  5152  axprlem4  5181  otsndisj  5262  otiunsndisj  5263  po2nr  5336  sotric  5350  sotrieq  5351  tz7.7  6053  fmptsnd  6752  fvtp1g  6785  f1cofveqaeqALT  6840  fsnex  6862  isocnv  6904  isores2  6907  isomin  6911  isoini  6912  f1oiso2  6926  ovmpodf  7120  offval  7232  ordsucun  7354  xp1st  7530  cnvf1olem  7610  fnse  7629  mpoxopoveq  7685  wfrlem3  7756  oalim  7955  omlim  7956  oaass  7984  omordi  7989  omwordri  7995  odi  8002  oen0  8009  oewordri  8015  nnawordi  8044  nnmordi  8054  omabs  8070  erinxp  8167  dom2lem  8342  mapen  8473  ssenen  8483  ssfi  8529  domfi  8530  domunfican  8582  mapfien  8662  ordtypelem6  8778  ordtypelem7  8779  card2inf  8810  inf3lem6  8886  cantnfle  8924  cantnflem1b  8939  cantnflem1  8942  wemapwe  8950  rankxplim3  9100  fseqenlem2  9241  dfac5lem4  9342  dfac2b  9346  cfsuc  9473  cfflb  9475  cofsmo  9485  infpssrlem4  9522  fin4en1  9525  ssfin4  9526  fin23lem26  9541  fin23lem22  9543  fin23lem27  9544  isf34lem4  9593  isf34lem5  9594  fin1a2lem12  9627  axdc3lem2  9667  axdc4lem  9671  ttukeylem6  9730  iundom2g  9756  pwcfsdom  9799  gchen2  9842  gchor  9843  fpwwe2lem7  9852  fpwwe2lem9  9854  fpwwe2lem11  9856  fpwwe2lem12  9857  fpwwe2  9859  pwfseqlem4  9878  gchina  9915  ltexprlem6  10257  prlem936  10263  mul4  10604  2addsub  10697  muladd  10869  ltleadd  10920  leord1  10964  eqord1  10965  ltord2  10966  leord2  10967  eqord2  10968  divmul3  11100  divcan7  11146  divadddiv  11152  lemul2a  11292  lemul12b  11294  ltmuldiv2  11311  ltdivmul  11312  ledivmul  11313  ltdivmul2  11314  lt2mul2div  11315  ledivmul2  11316  lemuldiv2  11318  lt2msq  11322  ltdiv23  11328  lediv23  11329  fimaxre  11381  supadd  11406  supmullem1  11408  cju  11431  zextlt  11866  suprzcl  11872  zmax  12156  xrlttr  12347  xrre3  12378  qbtwnre  12406  xrsupsslem  12513  xrinfmsslem  12514  supxrunb1  12525  supxrunb2  12526  ixxdisj  12566  iooshf  12628  icodisj  12675  iccf1o  12695  modid  13076  modadd1  13088  modmul1  13104  seqf1o  13223  expsub  13289  sqlecan  13383  bcval5  13490  hashmap  13603  hashfacen  13619  seqcoll  13629  swrdswrdlem  13880  cshwidxmod  14021  2cshwcshw  14043  cshwcshid  14045  resqreu  14467  lenegsq  14535  limsupbnd2  14695  icco1  14752  rlimresb  14777  rlimsqzlem  14860  rlimsqz  14861  rlimsqz2  14862  caucvgrlem  14884  fsum0diag2  14992  o1fsum  15022  ruclem8  15444  dvdsmulcr  15493  ndvdsadd  15615  bitsshft  15678  lcmdvds  15802  hashdvds  15962  eulerthlem2  15969  phisum  15977  pcqmul  16040  pcmpt  16078  prmreclem3  16104  4sqlem11  16141  0ram  16206  ramub1  16214  invfun  16886  initoeu2lem2  17127  coaval  17180  catcisolem  17218  funcestrcsetclem8  17249  fullestrcsetc  17253  embedsetcestrclem  17259  funcsetcestrclem8  17264  fullsetcestrc  17268  prfcl  17305  prf1st  17306  prf2nd  17307  1st2ndprf  17308  curfuncf  17340  isposd  17417  lubun  17585  isacs3lem  17628  pslem  17668  psss  17676  pwsdiagmhm  17831  gsumccat  17840  grpinvid1  17935  grpinvid2  17936  grplcan  17942  grpnpncan0  17976  dfgrp3lem  17978  dfgrp3  17979  grplactcnv  17983  0nsg  18102  eqger  18107  resghm  18139  conjghm  18154  subgga  18195  gaorber  18203  gastacl  18204  orbsta  18208  symgextf1lem  18303  psgnunilem2  18379  odid  18422  odmulg  18438  gexid  18461  odcau  18484  lsmssv  18523  lsmcom2  18535  pj1ghm  18581  frgpuptf  18650  frgpup1  18655  ghmplusg  18716  cyggex2  18765  gsumval3eu  18772  gsumval3  18775  ablfac1eu  18939  pgpfac1lem5  18945  isdrngd  19244  issrngd  19348  lmhmf1o  19534  lmhmima  19535  lmhmpreima  19536  lspextmo  19544  pwssplit2  19548  pwssplit3  19549  lspdisj  19613  islbs3  19643  lbsextlem4  19649  drngnidl  19717  lidldvgen  19743  issubassa2  19833  psrbagconf1o  19862  evlslem2  19999  ply1sclf1  20154  cnsubrg  20301  znunit  20406  cygznlem3  20412  dsmmsubg  20583  dsmmlss  20584  frlmsslsp  20636  frlmup1  20638  lindfrn  20661  f1lindf  20662  mamuass  20709  dmatmul  20804  dmatsubcl  20805  dmatmulcl  20807  dmatcrng  20809  scmataddcl  20823  scmatsubcl  20824  scmatcrng  20828  mdetunilem2  20920  pm2mpf1  21105  pm2mpghm  21122  eltg2  21264  ntrss  21361  opncldf1  21390  ssnei2  21422  neindisj  21423  restopnb  21481  restntr  21488  tgcmp  21707  hauscmplem  21712  2ndc1stc  21757  2ndcdisj  21762  2ndcomap  21764  restlly  21789  lly1stc  21802  isref  21815  islocfin  21823  comppfsc  21838  txcls  21910  txdis1cn  21941  pthaus  21944  txlm  21954  qtoptop2  22005  qtopomap  22024  kqt0lem  22042  pt1hmeo  22112  ptuncnv  22113  xkocnv  22120  fbasfip  22174  fgabs  22185  fbasrn  22190  elfm2  22254  fmfnfmlem2  22261  fmfnfmlem4  22263  ptcmplem3  22360  ptcmplem4  22361  tsmsres  22449  tsmsxplem1  22458  utoptop  22540  elbl2ps  22696  elbl2  22697  blin  22728  xmeter  22740  xmetresbl  22744  stdbdxmet  22822  metrest  22831  metustexhalf  22863  dscmet  22879  nrmmetd  22881  tngngp2  22958  nmoi2  23036  icccmplem2  23128  reconnlem2  23132  metdstri  23156  metdsle  23157  metdsre  23158  metnrmlem3  23166  fsumcn  23175  icccvx  23251  bndth  23259  evth  23260  reparphti  23298  pi1blem  23340  tcphcph  23537  iscfil2  23566  cfilfcls  23574  iscau4  23579  iscauf  23580  caucfil  23583  cncmet  23622  minveclem7  23735  ovoliunlem1  23800  ovolicc2lem2  23816  ovolicc2lem3  23817  ovolicc2lem4  23818  ovolicc2lem5  23819  ovolicc2  23820  voliunlem3  23850  voliun  23852  ioombl  23863  volivth  23905  ismbfd  23937  ismbf3d  23952  itg1addlem1  23990  i1fadd  23993  itg1addlem4  23997  itg2split  24047  itg2monolem1  24048  itg2gt0  24058  ibllem  24062  itgvallem3  24083  iblposlem  24089  dvmptfsum  24269  rolle  24284  dvlip  24287  c1liplem1  24290  lhop1  24308  lhop2  24309  dvcvx  24314  dvfsumge  24316  dvfsumrlimge0  24324  dvfsumrlim  24325  dvfsum2  24328  mdegaddle  24365  mdegvscale  24366  mdegmullem  24369  ply1divex  24427  coeeulem  24511  plyco  24528  dgrlt  24553  vieta1  24598  ulmss  24682  ulmdvlem3  24687  iblulm  24692  tanord  24817  eff1olem  24827  logdivlt  24899  logccv  24941  lawcos  25089  leibpilem1OLD  25214  xrlimcnp  25242  cxp2limlem  25249  cxp2lim  25250  cxploglim2  25252  divsqrtsumo1  25257  lgambdd  25310  sqff1o  25455  dvdsppwf1o  25459  dvdsflf1o  25460  musum  25464  muinv  25466  fsumdvdsmul  25468  sgmmul  25473  fsumvma  25485  logfac2  25489  chpchtsum  25491  logfacrlim  25496  logexprlim  25497  dchrelbas3  25510  dchrmulcl  25521  bposlem1  25556  lgsdchr  25627  lgsquadlem1  25652  lgsquadlem2  25653  lgsquad2lem2  25657  chebbnd1lem1  25741  chpchtlim  25751  rplogsumlem2  25757  dchrmusum2  25766  dchrvmasumlem1  25767  dchrvmasum2lem  25768  dchrvmasumlem2  25770  dchrvmasumlem3  25771  dchrvmasumiflem2  25774  dchrisum0flb  25782  dchrisum0fno1  25783  rpvmasum2  25784  dchrisum0re  25785  dchrisum0lem1  25788  dchrisum0lem2a  25789  dchrisum0lem2  25790  dchrisum0lem3  25791  rplogsum  25799  mulogsum  25804  mulog2sumlem2  25807  vmalogdivsum2  25810  2vmadivsumlem  25812  selberglem2  25818  selberg3lem1  25829  selberg4lem1  25832  selberg4  25833  pntrsumo1  25837  selberg34r  25843  pntrlog2bndlem1  25849  pntrlog2bndlem2  25850  pntrlog2bndlem3  25851  pntrlog2bndlem4  25852  pntrlog2bndlem5  25853  pntrlog2bndlem6  25855  pntibndlem3  25864  pntlemp  25882  ostthlem1  25899  ostth3  25910  ercgrg  25999  oppperpex  26235  axlowdimlem15  26439  axlowdimlem16  26440  axcontlem10  26456  cusgrfilem1  26934  upgriswlk  27119  crctcshwlkn0  27301  wwlksnextwrd  27382  wwlksnextwrdOLD  27387  clwlkclwwlklem2a  27498  grpoidinv  28056  grporcan  28066  grpoinvid1  28076  grpoinvid2  28077  grpolcan  28078  ablo4  28098  nvabs  28220  sspphOLD  28403  minvecolem7  28432  htthlem  28467  hvadd4  28586  hvaddsub4  28628  shscli  28869  pjspansn  29129  fh1  29170  fh2  29171  cm2j  29172  chscllem2  29190  spansncvi  29204  5oalem2  29207  5oalem5  29210  5oalem6  29211  3oalem2  29215  hoadd4  29336  cnvunop  29470  bralnfn  29500  eighmorth  29516  hmops  29572  hmopm  29573  adjlnop  29638  adjmul  29644  adjadd  29645  nmopcoi  29647  kbass5  29672  kbass6  29673  hstle  29782  stlesi  29793  mdsl0  29862  mdexchi  29887  atom1d  29905  superpos  29906  cvexchlem  29920  atomli  29934  atcvatlem  29937  chirredlem2  29943  chirredlem3  29944  atcvat4i  29949  mdsymlem1  29955  mdsymlem3  29957  mdsymlem5  29959  mdsymlem6  29960  sumdmdlem  29970  sumdmdlem2  29971  cdj1i  29985  opeldifid  30109  isoun  30183  1stpreimas  30187  f1od2  30203  archirngz  30475  archiabllem1  30479  archiabllem2c  30481  rngurd  30527  indf1ofs  30920  esum2d  30987  cntmeas  31121  ddemeas  31131  carsgclctunlem1  31211  itgeq12dv  31220  eulerpartlemgc  31256  eulerpartlemb  31262  eulerpartlemgs2  31274  ballotlemfc0  31387  ballotlemfcc  31388  signstfvneq0  31480  reprss  31527  reprpmtf1o  31536  hgt750lemb  31566  bnj607  31826  derangenlem  31993  subfacp1lem3  32004  subfacp1lem5  32006  cvmliftmolem2  32104  cvmliftlem6  32112  cvmlift2lem5  32129  cvmlift2lem7  32131  cvmlift2lem9  32133  mppspstlem  32308  dfon2lem6  32523  frrlem3  32616  frrlem13  32626  sltres  32660  noresle  32691  nosupno  32694  colinbtwnle  33070  finminlem  33157  nn0prpwlem  33161  isfne  33178  neibastop1  33198  neibastop2lem  33199  neibastop3  33201  tailfb  33216  onsuct0  33279  nndivsub  33295  knoppcnlem6  33327  knoppndvlem9  33349  knoppndvlem18  33358  knoppndvlem21  33361  bj-finsumval0  33995  rdgeqoa  34058  pibt2  34104  lindsadd  34304  matunitlindflem2  34308  poimirlem4  34315  poimirlem11  34322  poimirlem12  34323  poimirlem13  34324  poimirlem25  34336  poimirlem28  34339  heicant  34346  mblfinlem2  34349  mblfinlem3  34350  mblfinlem4  34351  mbfposadd  34358  itg2addnclem3  34364  bddiblnc  34381  ftc1anclem5  34390  ftc1anclem6  34391  ftc1anclem7  34392  ftc1anc  34394  frinfm  34430  filbcmb  34435  seqpo  34442  sstotbnd2  34472  isbndx  34480  ssbnd  34486  prdsbnd  34491  ismtycnv  34500  ismtyres  34506  heiborlem3  34511  heibor  34519  ghomdiv  34590  grpokerinj  34591  isdrngo2  34656  rngohomco  34672  rngoisocnv  34679  rngoisoco  34680  crngm4  34701  crngohomfo  34704  isidlc  34713  ispridl2  34736  ispridlc  34768  prtlem16  35428  ax12eq  35500  ax12el  35501  lshpcmp  35547  omllaw3  35804  omlfh1N  35817  cvratlem  35980  cvrat3  36001  cvrat4  36002  ps-2  36037  elpaddn0  36359  paddasslem10  36388  cdleme0cp  36773  cdleme32a  37000  cdlemeg49lebilem  37098  cdleme50eq  37100  tendoeq2  37333  diaglbN  37614  diameetN  37615  diainN  37616  dvhopN  37675  djaclN  37695  djajN  37696  dihopelvalcpre  37807  dih1dimatlem  37888  dihmeetcl  37904  djhcl  37959  mapdpglem2  38232  frlmsnic  38564  0prjspn  38655  ismrc  38671  eldioph2  38732  lzenom  38740  rexrabdioph  38765  fphpdo  38788  irrapxlem3  38795  elpell14qr2  38833  pell14qrreccl  38835  pell14qrdich  38840  pellfundglb  38856  monotoddzzfi  38913  2nn0ind  38916  jm2.21  38965  jm2.22  38966  dnnumch3  39021  dnwech  39022  fnwe2lem2  39025  hbtlem6  39103  imo72b2lem1  39864  mnuprdlem1  39961  mnuprdlem2  39962  ablsimpgfind  40023  cncmpmax  40685  disjf1  40846  eliccelioc  41207  fprodexp  41285  fprodabs2  41286  mullimc  41307  mullimcf  41314  islpcn  41330  limsuppnfdlem  41392  liminfval2  41459  xlimmnfvlem1  41523  xlimmnfvlem2  41524  xlimpnfvlem1  41527  xlimpnfvlem2  41528  cncfshift  41566  cncfperiod  41571  fprodcncf  41593  dvnprodlem1  41640  dvnprodlem2  41641  stoweidlem34  41729  stoweidlem48  41743  stoweidlem60  41755  fourierdlem42  41844  fourierdlem60  41861  fourierdlem61  41862  fourierdlem63  41864  fourierdlem65  41866  fourierdlem87  41888  fourierdlem97  41898  elaa2  41929  etransclem46  41975  etransc  41978  sge0iunmptlemfi  42105  isomennd  42223  ovnsslelem  42252  ovolval4lem2  42342  ovolval5lem3  42346  smflimlem3  42459  smflimlem4  42460  smflimlem6  42462  smfpimbor1lem1  42483  smflimmpt  42494  smflimsupmpt  42513  smfliminfmpt  42516  icceuelpart  42947  prproropf1olem4  43010  fmtnoprmfac2  43071  bgoldbtbndlem2  43313  bgoldbtbndlem3  43314  srhmsubc  43685  srhmsubcALTV  43703  aacllem  44243