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  5362  otsndisj  5492  otiunsndisj  5493  po2nr  5573  sotric  5589  sotrieq  5590  tz7.7  6387  fmptsnd  7172  fvtp1g  7201  f1cofveqaeqALT  7260  fsnex  7289  isocnv  7336  isores2  7339  isomin  7343  isoini  7344  f1oiso2  7358  ovmpodf  7574  offval  7700  ordsucun  7834  xp1st  8031  cnvf1olem  8119  fnse  8143  sexp2  8156  mpoxopoveq  8229  frrlem3  8299  frrlem13  8309  oalim  8533  omlim  8534  oaass  8562  omordi  8567  omwordri  8573  odi  8580  oen0  8588  oewordri  8594  nnawordi  8623  nnmordi  8633  omabs  8653  coflton  8673  nadd4  8701  erinxp  8805  dom2lem  9012  domssl  9018  mapen  9153  ssenen  9163  ssfiALT  9182  domfi  9197  php  9215  fissorduni  9275  domunfican  9306  mapfien  9393  ordtypelem6  9510  ordtypelem7  9511  card2inf  9542  inf3lem6  9627  cantnfle  9665  cantnflem1b  9680  cantnflem1  9683  wemapwe  9691  ttrclselem2  9720  rankxplim3  9891  fseqenlem2  10097  dfac5lem4  10198  dfac2b  10202  cfsuc  10328  cfflb  10330  cofsmo  10340  infpssrlem4  10377  fin4en1  10380  ssfin4  10381  fin23lem26  10396  fin23lem22  10398  fin23lem27  10399  isf34lem4  10448  isf34lem5  10449  fin1a2lem12  10482  axdc3lem2  10522  axdc4lem  10526  ttukeylem6  10585  iundom2g  10617  pwcfsdom  10661  gchen2  10704  gchor  10705  fpwwe2lem6  10714  fpwwe2lem8  10716  fpwwe2lem10  10718  fpwwe2lem11  10719  fpwwe2  10721  pwfseqlem4  10740  gchina  10777  ltexprlem6  11119  prlem936  11125  mul4  11471  2addsub  11564  muladd  11741  ltleadd  11792  leord1  11836  eqord1  11837  ltord2  11838  leord2  11839  eqord2  11840  divmul3  11972  divcan7  12019  divadddiv  12025  lemul2a  12165  lemul12b  12167  ltmuldiv2  12184  ltdivmul  12185  ledivmul  12186  ltdivmul2  12187  lt2mul2div  12188  ledivmul2  12189  lemuldiv2  12191  lt2msq  12195  ltdiv23  12201  lediv23  12202  fimaxre  12254  supadd  12278  supmullem1  12280  cju  12309  zextlt  12766  suprzcl  12772  zmax  13065  xrlttr  13262  xrre3  13294  qbtwnre  13322  xrsupsslem  13430  xrinfmsslem  13431  supxrunb1  13442  supxrunb2  13443  ixxdisj  13484  iooshf  13550  icodisj  13600  iccf1o  13620  modid  14029  modadd1  14041  modmul1  14060  seqf1o  14179  expsub  14246  sqlecan  14346  bcval5  14455  hashmap  14573  hashfacen  14592  seqcoll  14602  ccatf1  14729  swrdswrdlem  14846  swrdccatin2  14871  cshwidxmod  14947  2cshwcshw  14969  cshwcshid  14971  resqreu  15412  lenegsq  15481  limsupbnd2  15643  icco1  15700  rlimresb  15725  rlimsqzlem  15809  rlimsqz  15810  rlimsqz2  15811  caucvgrlem  15833  fsum0diag2  15942  o1fsum  15973  ruclem8  16398  dvdsmulcr  16448  ndvdsadd  16573  bitsshft  16638  lcmdvds  16776  hashdvds  16945  eulerthlem2  16952  phisum  16961  pcqmul  17024  pcmpt  17063  prmreclem3  17089  4sqlem11  17126  0ram  17191  ramub1  17199  invfun  17932  initoeu2lem2  18183  coaval  18236  catcisolem  18278  funcestrcsetclem8  18314  fullestrcsetc  18318  embedsetcestrclem  18324  funcsetcestrclem8  18329  fullsetcestrc  18333  prfcl  18370  prf1st  18371  prf2nd  18372  1st2ndprf  18373  curfuncf  18405  isposd  18489  lubun  18682  isacs3lem  18709  pslem  18739  psss  18747  chnccat  18793  chnpof1  18797  pwsdiagmhm  19020  grpinvid1  19195  grpinvid2  19196  grplcan  19204  grpnpncan0  19239  dfgrp3lem  19241  dfgrp3  19242  grplactcnv  19246  0nsg  19372  eqger  19383  qusxpid  19388  eqg0subg  19404  qus0subgadd  19407  resghm  19439  conjghm  19456  subgga  19507  gaorber  19515  gastacl  19516  orbsta  19520  symgextf1lem  19627  psgnunilem2  19702  odid  19745  odmulg  19763  gexid  19788  odcau  19811  lsmssv  19850  lsmcom2  19862  pj1ghm  19910  frgpuptf  19977  frgpup1  19982  ghmplusg  20053  cyggex2  20104  gsumval3eu  20111  gsumval3  20114  ablfac1eu  20282  pgpfac1lem5  20288  ablsimpgfind  20319  ringurd  20404  srhmsubc  20925  isdomn4  20960  isdrngd  21015  isdrngdOLD  21017  issrngd  21105  lmhmf1o  21314  lmhmima  21315  lmhmpreima  21316  lspextmo  21324  pwssplit2  21328  pwssplit3  21329  lspdisj  21396  islbs3  21426  lbsextlem4  21432  drngnidl  21524  rngqiprngghmlem2  21577  rngqiprnglinlem1  21580  rngqiprngghm  21588  lidldvgen  21651  cnsubrg  21726  znunit  21862  cygznlem3  21868  dsmmsubg  22042  dsmmlss  22043  frlmsslsp  22095  frlmup1  22097  lindfrn  22120  f1lindf  22121  issubassa2  22193  psrbagconf1o  22230  psrgrp  22257  evlslem2  22381  mhplss  22469  psdmul  22480  psdmvr  22483  ply1sclf1  22601  mamuass  22710  dmatmul  22805  dmatsubcl  22806  dmatmulcl  22808  dmatcrng  22810  scmataddcl  22824  scmatsubcl  22825  scmatcrng  22829  mdetunilem2  22921  matunitlindflem2  22988  pm2mpf1  23110  pm2mpghm  23127  eltg2  23269  ntrss  23366  opncldf1  23395  ssnei2  23427  neindisj  23428  restopnb  23486  restntr  23493  tgcmp  23712  hauscmplem  23717  2ndc1stc  23762  2ndcdisj  23768  2ndcomap  23770  restlly  23795  lly1stc  23808  isref  23821  islocfin  23829  comppfsc  23844  txcls  23916  txdis1cn  23947  pthaus  23950  txlm  23960  qtoptop2  24011  qtopomap  24030  kqt0lem  24048  pt1hmeo  24118  ptuncnv  24119  xkocnv  24126  fbasfip  24180  fgabs  24191  fbasrn  24196  elfm2  24260  fmfnfmlem2  24267  fmfnfmlem4  24269  ptcmplem3  24366  ptcmplem4  24367  tsmsres  24456  tsmsxplem1  24465  utoptop  24546  elbl2ps  24701  elbl2  24702  blin  24733  xmeter  24745  xmetresbl  24749  stdbdxmet  24827  metrest  24836  metustexhalf  24868  dscmet  24884  nrmmetd  24886  tngngp2  24964  nmoi2  25042  icccmplem2  25136  reconnlem2  25140  metdstri  25164  metdsle  25165  metdsre  25166  metnrmlem3  25174  fsumcn  25184  icccvx  25264  bndth  25272  evth  25273  reparphti  25311  pi1blem  25353  tcphcph  25551  iscfil2  25580  cfilfcls  25588  iscau4  25593  iscauf  25594  caucfil  25597  cncmet  25636  minveclem7  25749  ovoliunlem1  25816  ovolicc2lem2  25832  ovolicc2lem3  25833  ovolicc2lem4  25834  ovolicc2lem5  25835  ovolicc2  25836  voliunlem3  25866  voliun  25868  ioombl  25879  volivth  25921  ismbfd  25953  ismbf3d  25968  itg1addlem1  26006  i1fadd  26009  itg1addlem4  26013  itg2split  26063  itg2monolem1  26064  itg2gt0  26074  ibllem  26078  itgvallem3  26099  iblposlem  26105  bddiblnc  26155  dvmptfsum  26288  rolle  26303  dvlip  26306  c1liplem1  26309  lhop1  26327  lhop2  26328  dvcvx  26333  dvfsumge  26335  dvfsumrlimge0  26343  dvfsumrlim  26344  dvfsum2  26347  mdegaddle  26385  mdegvscale  26386  mdegmullem  26389  ply1divex  26448  coeeulem  26536  plyco  26553  dgrlt  26578  vieta1  26628  ulmss  26717  ulmdvlem3  26722  iblulm  26727  tanord  26859  eff1olem  26869  logdivlt  26942  logccv  26984  lawcos  27137  xrlimcnp  27289  cxp2limlem  27296  cxp2lim  27297  cxploglim2  27299  divsqrtsumo1  27304  lgambdd  27357  sqff1o  27502  dvdsppwf1o  27506  dvdsflf1o  27507  musum  27511  muinv  27513  fsumdvdsmul  27515  sgmmul  27521  fsumvma  27533  logfac2  27537  chpchtsum  27539  logfacrlim  27544  logexprlim  27545  dchrelbas3  27558  dchrmulcl  27569  bposlem1  27604  lgsdchr  27675  lgsquadlem1  27700  lgsquadlem2  27701  lgsquad2lem2  27705  chebbnd1lem1  27789  chpchtlim  27799  rplogsumlem2  27805  dchrmusum2  27814  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumiflem2  27822  dchrisum0flb  27830  dchrisum0fno1  27831  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  rplogsum  27847  mulogsum  27852  mulog2sumlem2  27855  vmalogdivsum2  27858  2vmadivsumlem  27860  selberglem2  27866  selberg3lem1  27877  selberg4lem1  27880  selberg4  27881  pntrsumo1  27885  selberg34r  27891  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntibndlem3  27912  pntlemp  27930  ostthlem1  27947  ostth3  27958  infdesc  27960  ltsres  28012  noresle  28047  nosupno  28053  nosupbday  28055  noinfno  28068  bday1  28193  cutlt  28311  addsproplem2  28349  negsproplem2  28408  mulsuniflem  28528  mulsunif2lem  28548  precsexlem9  28594  precsexlem10  28595  precsexlem11  28596  om2noseqlt  28678  om2noseqlt2  28679  om2noseqf1o  28680  om2noseqrdg  28683  noseqrdgfn  28685  bdaypw2n0bndlem  28842  bdayfinbndlem1  28846  recut  28873  elreno2  28874  renegscl  28877  ercgrg  28973  oppperpex  29222  axlowdimlem15  29527  axlowdimlem16  29528  axcontlem10  29544  cusgrfilem1  30029  upgriswlk  30214  crctcshwlkn0  30403  wwlksnext  30475  wwlksnextwrd  30479  clwlkclwwlklem2a  30582  wwlksext2clwwlk  30641  grpoidinv  31103  grporcan  31113  grpoinvid1  31123  grpoinvid2  31124  grpolcan  31125  ablo4  31145  nvabs  31267  minvecolem7  31478  htthlem  31512  hvadd4  31631  hvaddsub4  31673  shscli  31912  pjspansn  32172  fh1  32213  fh2  32214  cm2j  32215  chscllem2  32233  spansncvi  32247  5oalem2  32250  5oalem5  32253  5oalem6  32254  3oalem2  32258  hoadd4  32379  cnvunop  32513  bralnfn  32543  eighmorth  32559  hmops  32615  hmopm  32616  adjlnop  32681  adjmul  32687  adjadd  32688  nmopcoi  32690  kbass5  32715  kbass6  32716  hstle  32825  stlesi  32836  mdsl0  32905  mdexchi  32930  atom1d  32948  superpos  32949  cvexchlem  32963  atomli  32977  atcvatlem  32980  chirredlem2  32986  chirredlem3  32987  atcvat4i  32992  mdsymlem1  32998  mdsymlem3  33000  mdsymlem5  33002  mdsymlem6  33003  sumdmdlem  33013  sumdmdlem2  33014  cdj1i  33028  opeldifid  33186  isoun  33288  1stpreimas  33292  f1od2  33304  indf1ofs  33426  archirngz  33743  archiabllem1  33747  archiabllem2c  33749  esum2d  34718  cntmeas  34852  ddemeas  34862  carsgclctunlem1  34942  itgeq12dv  34951  eulerpartlemgc  34987  eulerpartlemb  34993  eulerpartlemgs2  35005  ballotlemfc0  35118  ballotlemfcc  35119  reprss  35239  reprpmtf1o  35248  hgt750lemb  35278  bnj607  35539  derangenlem  35915  subfacp1lem3  35926  subfacp1lem5  35928  cvmliftmolem2  36026  cvmliftlem6  36034  cvmlift2lem5  36051  cvmlift2lem7  36053  cvmlift2lem9  36055  mppspstlem  36315  dfon2lem6  36530  colinbtwnle  36863  nmulrid  36926  ltnadd  36947  nadddilem2  36950  nadddilem4  36952  finminlem  37086  nn0prpwlem  37090  isfne  37107  neibastop1  37127  neibastop2lem  37128  neibastop3  37130  tailfb  37145  onsuct0  37209  nndivsub  37225  knoppcnlem6  37344  knoppndvlem9  37366  knoppndvlem18  37375  knoppndvlem21  37378  bj-prmoore  38016  bj-finsumval0  38186  rdgeqoa  38273  pibt2  38320  lindsadd  38516  poimirlem4  38522  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem25  38543  poimirlem28  38546  heicant  38553  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  mbfposadd  38565  itg2addnclem3  38571  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anc  38599  frinfm  38649  filbcmb  38654  seqpo  38661  sstotbnd2  38688  isbndx  38696  ssbnd  38702  prdsbnd  38707  ismtycnv  38716  ismtyres  38722  heiborlem3  38727  heibor  38735  ghomdiv  38806  grpokerinj  38807  isdrngo2  38872  rngohomco  38888  rngoisocnv  38895  rngoisoco  38896  crngm4  38917  crngohomfo  38920  isidlc  38929  ispridl2  38952  ispridlc  38984  prtlem16  39906  ax12eq  39978  ax12el  39979  lshpcmp  40025  omllaw3  40282  omlfh1N  40295  cvratlem  40458  cvrat3  40479  cvrat4  40480  ps-2  40515  elpaddn0  40837  paddasslem10  40866  cdleme0cp  41251  cdleme32a  41478  cdlemeg49lebilem  41576  cdleme50eq  41578  tendoeq2  41811  diaglbN  42092  diameetN  42093  diainN  42094  dvhopN  42153  djaclN  42173  djajN  42174  dihopelvalcpre  42285  dih1dimatlem  42366  dihmeetcl  42382  djhcl  42437  mapdpglem2  42710  3factsumint1  43051  sticksstones22  43198  unitscyglem4  43228  imacrhmcl  43561  frlmsnic  43584  psrmnd  43587  evlselvlem  43596  fsuppind  43598  0prjspn  43644  ismrc  43691  eldioph2  43752  lzenom  43760  rexrabdioph  43780  fphpdo  43803  irrapxlem3  43810  elpell14qr2  43848  pell14qrreccl  43850  pell14qrdich  43855  pellfundglb  43871  monotoddzzfi  43928  2nn0ind  43931  jm2.21  43980  jm2.22  43981  dnnumch3  44033  dnwech  44034  fnwe2lem2  44037  hbtlem6  44115  cantnfresb  44310  imo72b2lem1  45154  mnuprdlem1  45241  mnuprdlem2  45242  relpmin  45920  traxext  45945  cncmpmax  46018  disjf1  46167  eliccelioc  46502  fprodexp  46575  fprodabs2  46576  mullimc  46597  mullimcf  46604  islpcn  46618  limsuppnfdlem  46680  liminfval2  46747  xlimmnfvlem1  46811  xlimmnfvlem2  46812  xlimpnfvlem1  46815  xlimpnfvlem2  46816  cncfshift  46853  cncfperiod  46858  fprodcncf  46879  dvnprodlem1  46925  dvnprodlem2  46926  stoweidlem34  47013  stoweidlem48  47027  stoweidlem60  47039  fourierdlem42  47128  fourierdlem60  47145  fourierdlem61  47146  fourierdlem63  47148  fourierdlem65  47150  fourierdlem87  47172  fourierdlem97  47182  elaa2  47213  etransclem46  47259  etransc  47262  salrestss  47340  sge0iunmptlemfi  47392  isomennd  47510  ovnsslelem  47539  ovolval4lem2  47629  smflimlem3  47752  smflimlem4  47753  smflimlem6  47755  smfpimbor1lem1  47777  smflimmpt  47789  smflimsupmpt  47808  smfliminfmpt  47811  fsetsnf1  48091  fcoresf1  48108  fvelsetpreimafv  48438  icceuelpart  48487  prproropf1olem4  48557  fmtnoprmfac2  48621  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  gpg3nbgrvtx0ALT  49144  gpg3nbgrvtx1  49145  srhmsubcALTV  49391  xpco2  49936  catprs  50088  uppropd  50258  thincciso2  50532  prsthinc  50541  functermc  50585  fulltermc  50588  lmdran  50748  cmdlan  50749  aacllem  50908