Theorem adantrr 723

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 599	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 208  df-an 397

This theorem is referenced by:  ad2antrl  734  ad2ant2r  753  ad2ant2lr  754  cases2ALT  1054  consensus  1058  3adant3  1138  3ad2antr1  1195  reusv2lem3  5336  axprlem4OLD  5366  otsndisj  5467  otiunsndisj  5468  po2nr  5547  sotric  5563  sotrieq  5564  tz7.7  6343  fmptsnd  7120  fvtp1g  7149  f1cofveqaeqALT  7209  fsnex  7234  isocnv  7281  isores2  7284  isomin  7288  isoini  7289  f1oiso2  7303  ovmpodf  7519  offval  7636  ordsucun  7772  xp1st  7970  cnvf1olem  8056  fnse  8080  sexp2  8093  mpoxopoveq  8166  frrlem3  8235  frrlem13  8245  oalim  8464  omlim  8465  oaass  8493  omordi  8498  omwordri  8504  odi  8511  oen0  8519  oewordri  8525  nnawordi  8554  nnmordi  8564  omabs  8584  coflton  8604  nadd4  8631  erinxp  8735  dom2lem  8936  domssl  8942  mapen  9076  ssenen  9086  ssfiALT  9105  domfi  9120  php  9138  domunfican  9229  mapfien  9318  ordtypelem6  9435  ordtypelem7  9436  card2inf  9467  inf3lem6  9552  cantnfle  9590  cantnflem1b  9605  cantnflem1  9608  wemapwe  9616  ttrclselem2  9645  rankxplim3  9803  fseqenlem2  9945  dfac5lem4  10046  dfac5lem4OLD  10048  dfac2b  10051  cfsuc  10177  cfflb  10179  cofsmo  10189  infpssrlem4  10226  fin4en1  10229  ssfin4  10230  fin23lem26  10245  fin23lem22  10247  fin23lem27  10248  isf34lem4  10297  isf34lem5  10298  fin1a2lem12  10331  axdc3lem2  10371  axdc4lem  10375  ttukeylem6  10434  iundom2g  10460  pwcfsdom  10504  gchen2  10547  gchor  10548  fpwwe2lem6  10557  fpwwe2lem8  10559  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2  10564  pwfseqlem4  10583  gchina  10620  ltexprlem6  10962  prlem936  10968  mul4  11312  2addsub  11405  muladd  11580  ltleadd  11631  leord1  11675  eqord1  11676  ltord2  11677  leord2  11678  eqord2  11679  divmul3  11812  divcan7  11862  divadddiv  11868  lemul2a  12008  lemul12b  12010  ltmuldiv2  12028  ltdivmul  12029  ledivmul  12030  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  lt2msq  12039  ltdiv23  12045  lediv23  12046  fimaxre  12098  supadd  12122  supmullem1  12124  cju  12153  zextlt  12601  suprzcl  12607  zmax  12893  xrlttr  13089  xrre3  13121  qbtwnre  13149  xrsupsslem  13257  xrinfmsslem  13258  supxrunb1  13269  supxrunb2  13270  ixxdisj  13311  iooshf  13377  icodisj  13427  iccf1o  13447  modid  13853  modadd1  13865  modmul1  13884  seqf1o  14003  expsub  14070  sqlecan  14169  bcval5  14278  hashmap  14395  hashfacen  14414  seqcoll  14424  swrdswrdlem  14664  swrdccatin2  14689  cshwidxmod  14763  2cshwcshw  14785  cshwcshid  14787  resqreu  15212  lenegsq  15281  limsupbnd2  15443  icco1  15500  rlimresb  15525  rlimsqzlem  15609  rlimsqz  15610  rlimsqz2  15611  caucvgrlem  15633  fsum0diag2  15743  o1fsum  15774  ruclem8  16202  dvdsmulcr  16252  ndvdsadd  16377  bitsshft  16442  lcmdvds  16575  hashdvds  16743  eulerthlem2  16750  phisum  16759  pcqmul  16822  pcmpt  16861  prmreclem3  16887  4sqlem11  16924  0ram  16989  ramub1  16997  invfun  17729  initoeu2lem2  17980  coaval  18033  catcisolem  18075  funcestrcsetclem8  18111  fullestrcsetc  18115  embedsetcestrclem  18121  funcsetcestrclem8  18126  fullsetcestrc  18130  prfcl  18167  prf1st  18168  prf2nd  18169  1st2ndprf  18170  curfuncf  18202  isposd  18286  lubun  18479  isacs3lem  18506  pslem  18536  psss  18544  chnccat  18590  chnpof1  18594  pwsdiagmhm  18797  grpinvid1  18965  grpinvid2  18966  grplcan  18974  grpnpncan0  19010  dfgrp3lem  19012  dfgrp3  19013  grplactcnv  19017  0nsg  19142  eqger  19151  eqg0subg  19169  qus0subgadd  19172  resghm  19205  conjghm  19222  subgga  19273  gaorber  19281  gastacl  19282  orbsta  19286  symgextf1lem  19393  psgnunilem2  19468  odid  19511  odmulg  19529  gexid  19554  odcau  19577  lsmssv  19616  lsmcom2  19628  pj1ghm  19676  frgpuptf  19743  frgpup1  19748  ghmplusg  19819  cyggex2  19870  gsumval3eu  19877  gsumval3  19880  ablfac1eu  20048  pgpfac1lem5  20054  ablsimpgfind  20085  ringurd  20164  srhmsubc  20659  isdomn4  20695  isdrngd  20744  isdrngdOLD  20746  issrngd  20834  lmhmf1o  21043  lmhmima  21044  lmhmpreima  21045  lspextmo  21053  pwssplit2  21057  pwssplit3  21058  lspdisj  21125  islbs3  21155  lbsextlem4  21161  drngnidl  21243  rngqiprngghmlem2  21288  rngqiprnglinlem1  21291  rngqiprngghm  21299  lidldvgen  21334  cnsubrg  21409  znunit  21545  cygznlem3  21551  dsmmsubg  21725  dsmmlss  21726  frlmsslsp  21778  frlmup1  21780  lindfrn  21803  f1lindf  21804  issubassa2  21874  psrbagconf1o  21911  psrgrp  21938  evlslem2  22062  mhplss  22150  psdmul  22161  psdmvr  22164  ply1sclf1  22282  mamuass  22392  dmatmul  22487  dmatsubcl  22488  dmatmulcl  22490  dmatcrng  22492  scmataddcl  22506  scmatsubcl  22507  scmatcrng  22511  mdetunilem2  22603  pm2mpf1  22789  pm2mpghm  22806  eltg2  22948  ntrss  23045  opncldf1  23074  ssnei2  23106  neindisj  23107  restopnb  23165  restntr  23172  tgcmp  23391  hauscmplem  23396  2ndc1stc  23441  2ndcdisj  23446  2ndcomap  23448  restlly  23473  lly1stc  23486  isref  23499  islocfin  23507  comppfsc  23522  txcls  23594  txdis1cn  23625  pthaus  23628  txlm  23638  qtoptop2  23689  qtopomap  23708  kqt0lem  23726  pt1hmeo  23796  ptuncnv  23797  xkocnv  23804  fbasfip  23858  fgabs  23869  fbasrn  23874  elfm2  23938  fmfnfmlem2  23945  fmfnfmlem4  23947  ptcmplem3  24044  ptcmplem4  24045  tsmsres  24134  tsmsxplem1  24143  utoptop  24224  elbl2ps  24379  elbl2  24380  blin  24411  xmeter  24423  xmetresbl  24427  stdbdxmet  24505  metrest  24514  metustexhalf  24546  dscmet  24562  nrmmetd  24564  tngngp2  24642  nmoi2  24720  icccmplem2  24814  reconnlem2  24818  metdstri  24842  metdsle  24843  metdsre  24844  metnrmlem3  24852  fsumcn  24862  icccvx  24942  bndth  24950  evth  24951  reparphti  24989  pi1blem  25031  tcphcph  25229  iscfil2  25258  cfilfcls  25266  iscau4  25271  iscauf  25272  caucfil  25275  cncmet  25314  minveclem7  25427  ovoliunlem1  25494  ovolicc2lem2  25510  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2lem5  25513  ovolicc2  25514  voliunlem3  25544  voliun  25546  ioombl  25557  volivth  25599  ismbfd  25631  ismbf3d  25646  itg1addlem1  25684  i1fadd  25687  itg1addlem4  25691  itg2split  25741  itg2monolem1  25742  itg2gt0  25752  ibllem  25756  itgvallem3  25778  iblposlem  25784  bddiblnc  25834  dvmptfsum  25967  rolle  25982  dvlip  25985  c1liplem1  25988  lhop1  26006  lhop2  26007  dvcvx  26012  dvfsumge  26014  dvfsumrlimge0  26022  dvfsumrlim  26023  dvfsum2  26026  mdegaddle  26064  mdegvscale  26065  mdegmullem  26068  ply1divex  26127  coeeulem  26214  plyco  26231  dgrlt  26256  vieta1  26303  ulmss  26387  ulmdvlem3  26392  iblulm  26397  tanord  26527  eff1olem  26537  logdivlt  26610  logccv  26652  lawcos  26805  xrlimcnp  26957  cxp2limlem  26964  cxp2lim  26965  cxploglim2  26967  divsqrtsumo1  26972  lgambdd  27025  sqff1o  27170  dvdsppwf1o  27174  dvdsflf1o  27175  musum  27179  muinv  27181  fsumdvdsmul  27183  sgmmul  27189  fsumvma  27201  logfac2  27205  chpchtsum  27207  logfacrlim  27212  logexprlim  27213  dchrelbas3  27226  dchrmulcl  27237  bposlem1  27272  lgsdchr  27343  lgsquadlem1  27368  lgsquadlem2  27369  lgsquad2lem2  27373  chebbnd1lem1  27457  chpchtlim  27467  rplogsumlem2  27473  dchrmusum2  27482  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrvmasumlem2  27486  dchrvmasumlem3  27487  dchrvmasumiflem2  27490  dchrisum0flb  27498  dchrisum0fno1  27499  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  rplogsum  27515  mulogsum  27520  mulog2sumlem2  27523  vmalogdivsum2  27526  2vmadivsumlem  27528  selberglem2  27534  selberg3lem1  27545  selberg4lem1  27548  selberg4  27549  pntrsumo1  27553  selberg34r  27559  pntrlog2bndlem1  27565  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntibndlem3  27580  pntlemp  27598  ostthlem1  27615  ostth3  27626  ltsres  27651  noresle  27686  nosupno  27692  nosupbday  27694  noinfno  27707  bday1  27831  cutlt  27949  addsproplem2  27987  negsproplem2  28046  mulsuniflem  28166  mulsunif2lem  28186  precsexlem9  28232  precsexlem10  28233  precsexlem11  28234  om2noseqlt  28316  om2noseqlt2  28317  om2noseqf1o  28318  om2noseqrdg  28321  noseqrdgfn  28323  bdaypw2n0bndlem  28480  bdayfinbndlem1  28484  recut  28511  elreno2  28512  renegscl  28515  ercgrg  28610  oppperpex  28846  axlowdimlem15  29050  axlowdimlem16  29051  axcontlem10  29067  cusgrfilem1  29549  upgriswlk  29734  crctcshwlkn0  29914  wwlksnext  29986  wwlksnextwrd  29990  clwlkclwwlklem2a  30093  wwlksext2clwwlk  30152  grpoidinv  30604  grporcan  30614  grpoinvid1  30624  grpoinvid2  30625  grpolcan  30626  ablo4  30646  nvabs  30768  minvecolem7  30979  htthlem  31013  hvadd4  31132  hvaddsub4  31174  shscli  31413  pjspansn  31673  fh1  31714  fh2  31715  cm2j  31716  chscllem2  31734  spansncvi  31748  5oalem2  31751  5oalem5  31754  5oalem6  31755  3oalem2  31759  hoadd4  31880  cnvunop  32014  bralnfn  32044  eighmorth  32060  hmops  32116  hmopm  32117  adjlnop  32182  adjmul  32188  adjadd  32189  nmopcoi  32191  kbass5  32216  kbass6  32217  hstle  32326  stlesi  32337  mdsl0  32406  mdexchi  32431  atom1d  32449  superpos  32450  cvexchlem  32464  atomli  32478  atcvatlem  32481  chirredlem2  32487  chirredlem3  32488  atcvat4i  32493  mdsymlem1  32499  mdsymlem3  32501  mdsymlem5  32503  mdsymlem6  32504  sumdmdlem  32514  sumdmdlem2  32515  cdj1i  32529  opeldifid  32695  isoun  32801  1stpreimas  32805  f1od2  32818  indf1ofs  32952  ccatf1  33035  archirngz  33277  archiabllem1  33281  archiabllem2c  33283  qusxpid  33453  esum2d  34284  cntmeas  34417  ddemeas  34427  carsgclctunlem1  34508  itgeq12dv  34517  eulerpartlemgc  34553  eulerpartlemb  34559  eulerpartlemgs2  34571  ballotlemfc0  34684  ballotlemfcc  34685  reprss  34808  reprpmtf1o  34817  hgt750lemb  34847  bnj607  35105  fissorduni  35278  derangenlem  35406  subfacp1lem3  35417  subfacp1lem5  35419  cvmliftmolem2  35517  cvmliftlem6  35525  cvmlift2lem5  35542  cvmlift2lem7  35544  cvmlift2lem9  35546  mppspstlem  35806  dfon2lem6  36021  colinbtwnle  36353  finminlem  36553  nn0prpwlem  36557  isfne  36574  neibastop1  36594  neibastop2lem  36595  neibastop3  36597  tailfb  36612  onsuct0  36676  nndivsub  36692  mh-inf3f1  36776  knoppcnlem6  36811  knoppndvlem9  36833  knoppndvlem18  36842  knoppndvlem21  36845  bj-prmoore  37480  bj-finsumval0  37652  rdgeqoa  37739  pibt2  37786  lindsadd  37987  matunitlindflem2  37991  poimirlem4  37998  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem25  38019  poimirlem28  38022  heicant  38029  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  mbfposadd  38041  itg2addnclem3  38047  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anc  38075  frinfm  38109  filbcmb  38114  seqpo  38121  sstotbnd2  38148  isbndx  38156  ssbnd  38162  prdsbnd  38167  ismtycnv  38176  ismtyres  38182  heiborlem3  38187  heibor  38195  ghomdiv  38266  grpokerinj  38267  isdrngo2  38332  rngohomco  38348  rngoisocnv  38355  rngoisoco  38356  crngm4  38377  crngohomfo  38380  isidlc  38389  ispridl2  38412  ispridlc  38444  prtlem16  39368  ax12eq  39440  ax12el  39441  lshpcmp  39487  omllaw3  39744  omlfh1N  39757  cvratlem  39920  cvrat3  39941  cvrat4  39942  ps-2  39977  elpaddn0  40299  paddasslem10  40328  cdleme0cp  40713  cdleme32a  40940  cdlemeg49lebilem  41038  cdleme50eq  41040  tendoeq2  41273  diaglbN  41554  diameetN  41555  diainN  41556  dvhopN  41615  djaclN  41635  djajN  41636  dihopelvalcpre  41747  dih1dimatlem  41828  dihmeetcl  41844  djhcl  41899  mapdpglem2  42172  3factsumint1  42513  sticksstones22  42660  unitscyglem4  42690  imacrhmcl  43011  frlmsnic  43033  psrmnd  43036  evlselvlem  43045  fsuppind  43047  0prjspn  43085  infdesc  43100  ismrc  43157  eldioph2  43218  lzenom  43226  rexrabdioph  43246  fphpdo  43269  irrapxlem3  43276  elpell14qr2  43314  pell14qrreccl  43316  pell14qrdich  43321  pellfundglb  43337  monotoddzzfi  43394  2nn0ind  43397  jm2.21  43446  jm2.22  43447  dnnumch3  43499  dnwech  43500  fnwe2lem2  43503  hbtlem6  43581  cantnfresb  43776  imo72b2lem1  44620  mnuprdlem1  44723  mnuprdlem2  44724  relpmin  45403  traxext  45428  cncmpmax  45487  disjf1  45637  eliccelioc  45973  fprodexp  46046  fprodabs2  46047  mullimc  46068  mullimcf  46075  islpcn  46089  limsuppnfdlem  46151  liminfval2  46218  xlimmnfvlem1  46282  xlimmnfvlem2  46283  xlimpnfvlem1  46286  xlimpnfvlem2  46287  cncfshift  46324  cncfperiod  46329  fprodcncf  46350  dvnprodlem1  46396  dvnprodlem2  46397  stoweidlem34  46484  stoweidlem48  46498  stoweidlem60  46510  fourierdlem42  46599  fourierdlem60  46616  fourierdlem61  46617  fourierdlem63  46619  fourierdlem65  46621  fourierdlem87  46643  fourierdlem97  46653  elaa2  46684  etransclem46  46730  etransc  46733  salrestss  46811  sge0iunmptlemfi  46863  isomennd  46981  ovnsslelem  47010  ovolval4lem2  47100  smflimlem3  47223  smflimlem4  47224  smflimlem6  47226  smfpimbor1lem1  47248  smflimmpt  47260  smflimsupmpt  47279  smfliminfmpt  47282  fsetsnf1  47522  fcoresf1  47539  fvelsetpreimafv  47869  icceuelpart  47918  prproropf1olem4  47988  fmtnoprmfac2  48052  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  gpgnbgrvtx0  48572  gpgnbgrvtx1  48573  gpg3nbgrvtx0ALT  48575  gpg3nbgrvtx1  48576  srhmsubcALTV  48823  xpco2  49354  catprs  49508  uppropd  49678  thincciso2  49952  prsthinc  49961  functermc  50005  fulltermc  50008  lmdran  50168  cmdlan  50169  aacllem  50298