Theorem adantrr 714

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 593	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 206  df-an 397

This theorem is referenced by:  ad2antrl  725  ad2ant2r  744  ad2ant2lr  745  cases2ALT  1046  consensus  1050  3adant3  1131  3ad2antr1  1187  reusv2lem3  5338  axprlem4  5364  otsndisj  5452  otiunsndisj  5453  po2nr  5535  sotric  5549  sotrieq  5550  tz7.7  6315  fmptsnd  7081  fvtp1g  7113  f1cofveqaeqALT  7172  fsnex  7195  isocnv  7241  isores2  7244  isomin  7248  isoini  7249  f1oiso2  7263  ovmpodf  7471  offval  7584  ordsucun  7717  xp1st  7910  cnvf1olem  7997  fnse  8020  mpoxopoveq  8084  frrlem3  8153  frrlem13  8163  wfrlem3OLD  8190  oalim  8412  omlim  8413  oaass  8442  omordi  8447  omwordri  8453  odi  8460  oen0  8467  oewordri  8473  nnawordi  8502  nnmordi  8512  omabs  8531  erinxp  8630  dom2lem  8832  domssl  8838  mapen  8985  ssenen  8995  ssfiALT  9018  domfi  9036  php  9054  domunfican  9164  mapfien  9244  ordtypelem6  9359  ordtypelem7  9360  card2inf  9391  inf3lem6  9469  cantnfle  9507  cantnflem1b  9522  cantnflem1  9525  wemapwe  9533  ttrclselem2  9562  rankxplim3  9717  fseqenlem2  9861  dfac5lem4  9962  dfac2b  9966  cfsuc  10093  cfflb  10095  cofsmo  10105  infpssrlem4  10142  fin4en1  10145  ssfin4  10146  fin23lem26  10161  fin23lem22  10163  fin23lem27  10164  isf34lem4  10213  isf34lem5  10214  fin1a2lem12  10247  axdc3lem2  10287  axdc4lem  10291  ttukeylem6  10350  iundom2g  10376  pwcfsdom  10419  gchen2  10462  gchor  10463  fpwwe2lem6  10472  fpwwe2lem8  10474  fpwwe2lem10  10476  fpwwe2lem11  10477  fpwwe2  10479  pwfseqlem4  10498  gchina  10535  ltexprlem6  10877  prlem936  10883  mul4  11223  2addsub  11315  muladd  11487  ltleadd  11538  leord1  11582  eqord1  11583  ltord2  11584  leord2  11585  eqord2  11586  divmul3  11718  divcan7  11764  divadddiv  11770  lemul2a  11910  lemul12b  11912  ltmuldiv2  11929  ltdivmul  11930  ledivmul  11931  ltdivmul2  11932  lt2mul2div  11933  ledivmul2  11934  lemuldiv2  11936  lt2msq  11940  ltdiv23  11946  lediv23  11947  fimaxre  11999  supadd  12023  supmullem1  12025  cju  12049  zextlt  12474  suprzcl  12480  zmax  12765  xrlttr  12954  xrre3  12985  qbtwnre  13013  xrsupsslem  13121  xrinfmsslem  13122  supxrunb1  13133  supxrunb2  13134  ixxdisj  13174  iooshf  13238  icodisj  13288  iccf1o  13308  modid  13696  modadd1  13708  modmul1  13724  seqf1o  13844  expsub  13911  sqlecan  14005  bcval5  14112  hashmap  14229  hashfacen  14245  hashfacenOLD  14246  seqcoll  14257  swrdswrdlem  14496  swrdccatin2  14521  cshwidxmod  14595  2cshwcshw  14617  cshwcshid  14619  resqreu  15043  lenegsq  15111  limsupbnd2  15271  icco1  15328  rlimresb  15353  rlimsqzlem  15439  rlimsqz  15440  rlimsqz2  15441  caucvgrlem  15463  fsum0diag2  15574  o1fsum  15604  ruclem8  16025  dvdsmulcr  16074  ndvdsadd  16198  bitsshft  16261  lcmdvds  16390  hashdvds  16553  eulerthlem2  16560  phisum  16568  pcqmul  16631  pcmpt  16670  prmreclem3  16696  4sqlem11  16733  0ram  16798  ramub1  16806  invfun  17553  initoeu2lem2  17807  coaval  17860  catcisolem  17902  funcestrcsetclem8  17941  fullestrcsetc  17945  embedsetcestrclem  17951  funcsetcestrclem8  17956  fullsetcestrc  17960  prfcl  17997  prf1st  17998  prf2nd  17999  1st2ndprf  18000  curfuncf  18033  isposd  18118  lubun  18310  isacs3lem  18337  pslem  18367  psss  18375  pwsdiagmhm  18546  grpinvid1  18706  grpinvid2  18707  grplcan  18713  grpnpncan0  18747  dfgrp3lem  18749  dfgrp3  18750  grplactcnv  18754  0nsg  18873  eqger  18882  resghm  18926  conjghm  18941  subgga  18982  gaorber  18990  gastacl  18991  orbsta  18995  symgextf1lem  19104  psgnunilem2  19179  odid  19222  odmulg  19239  gexid  19262  odcau  19285  lsmssv  19324  lsmcom2  19336  pj1ghm  19384  frgpuptf  19451  frgpup1  19456  ghmplusg  19522  cyggex2  19573  gsumval3eu  19580  gsumval3  19583  ablfac1eu  19751  pgpfac1lem5  19757  ablsimpgfind  19788  isdrngd  20098  issrngd  20204  lmhmf1o  20391  lmhmima  20392  lmhmpreima  20393  lspextmo  20401  pwssplit2  20405  pwssplit3  20406  lspdisj  20470  islbs3  20500  lbsextlem4  20506  drngnidl  20583  lidldvgen  20609  cnsubrg  20741  znunit  20854  cygznlem3  20860  dsmmsubg  21033  dsmmlss  21034  frlmsslsp  21086  frlmup1  21088  lindfrn  21111  f1lindf  21112  issubassa2  21179  psrbagconf1o  21222  psrbagconf1oOLD  21223  evlslem2  21372  mhplss  21428  ply1sclf1  21543  mamuass  21632  dmatmul  21729  dmatsubcl  21730  dmatmulcl  21732  dmatcrng  21734  scmataddcl  21748  scmatsubcl  21749  scmatcrng  21753  mdetunilem2  21845  pm2mpf1  22031  pm2mpghm  22048  eltg2  22191  ntrss  22289  opncldf1  22318  ssnei2  22350  neindisj  22351  restopnb  22409  restntr  22416  tgcmp  22635  hauscmplem  22640  2ndc1stc  22685  2ndcdisj  22690  2ndcomap  22692  restlly  22717  lly1stc  22730  isref  22743  islocfin  22751  comppfsc  22766  txcls  22838  txdis1cn  22869  pthaus  22872  txlm  22882  qtoptop2  22933  qtopomap  22952  kqt0lem  22970  pt1hmeo  23040  ptuncnv  23041  xkocnv  23048  fbasfip  23102  fgabs  23113  fbasrn  23118  elfm2  23182  fmfnfmlem2  23189  fmfnfmlem4  23191  ptcmplem3  23288  ptcmplem4  23289  tsmsres  23378  tsmsxplem1  23387  utoptop  23469  elbl2ps  23625  elbl2  23626  blin  23657  xmeter  23669  xmetresbl  23673  stdbdxmet  23754  metrest  23763  metustexhalf  23795  dscmet  23811  nrmmetd  23813  tngngp2  23899  nmoi2  23977  icccmplem2  24069  reconnlem2  24073  metdstri  24097  metdsle  24098  metdsre  24099  metnrmlem3  24107  fsumcn  24116  icccvx  24196  bndth  24204  evth  24205  reparphti  24243  pi1blem  24285  tcphcph  24484  iscfil2  24513  cfilfcls  24521  iscau4  24526  iscauf  24527  caucfil  24530  cncmet  24569  minveclem7  24682  ovoliunlem1  24749  ovolicc2lem2  24765  ovolicc2lem3  24766  ovolicc2lem4  24767  ovolicc2lem5  24768  ovolicc2  24769  voliunlem3  24799  voliun  24801  ioombl  24812  volivth  24854  ismbfd  24886  ismbf3d  24901  itg1addlem1  24939  i1fadd  24942  itg1addlem4  24946  itg1addlem4OLD  24947  itg2split  24997  itg2monolem1  24998  itg2gt0  25008  ibllem  25012  itgvallem3  25033  iblposlem  25039  bddiblnc  25089  dvmptfsum  25222  rolle  25237  dvlip  25240  c1liplem1  25243  lhop1  25261  lhop2  25262  dvcvx  25267  dvfsumge  25269  dvfsumrlimge0  25277  dvfsumrlim  25278  dvfsum2  25281  mdegaddle  25322  mdegvscale  25323  mdegmullem  25326  ply1divex  25384  coeeulem  25468  plyco  25485  dgrlt  25510  vieta1  25555  ulmss  25639  ulmdvlem3  25644  iblulm  25649  tanord  25777  eff1olem  25787  logdivlt  25859  logccv  25901  lawcos  26049  xrlimcnp  26201  cxp2limlem  26208  cxp2lim  26209  cxploglim2  26211  divsqrtsumo1  26216  lgambdd  26269  sqff1o  26414  dvdsppwf1o  26418  dvdsflf1o  26419  musum  26423  muinv  26425  fsumdvdsmul  26427  sgmmul  26432  fsumvma  26444  logfac2  26448  chpchtsum  26450  logfacrlim  26455  logexprlim  26456  dchrelbas3  26469  dchrmulcl  26480  bposlem1  26515  lgsdchr  26586  lgsquadlem1  26611  lgsquadlem2  26612  lgsquad2lem2  26616  chebbnd1lem1  26700  chpchtlim  26710  rplogsumlem2  26716  dchrmusum2  26725  dchrvmasumlem1  26726  dchrvmasum2lem  26727  dchrvmasumlem2  26729  dchrvmasumlem3  26730  dchrvmasumiflem2  26733  dchrisum0flb  26741  dchrisum0fno1  26742  rpvmasum2  26743  dchrisum0re  26744  dchrisum0lem1  26747  dchrisum0lem2a  26748  dchrisum0lem2  26749  dchrisum0lem3  26750  rplogsum  26758  mulogsum  26763  mulog2sumlem2  26766  vmalogdivsum2  26769  2vmadivsumlem  26771  selberglem2  26777  selberg3lem1  26788  selberg4lem1  26791  selberg4  26792  pntrsumo1  26796  selberg34r  26802  pntrlog2bndlem1  26808  pntrlog2bndlem2  26809  pntrlog2bndlem3  26810  pntrlog2bndlem4  26811  pntrlog2bndlem5  26812  pntrlog2bndlem6  26814  pntibndlem3  26823  pntlemp  26841  ostthlem1  26858  ostth3  26869  sltres  26893  ercgrg  27014  oppperpex  27250  axlowdimlem15  27460  axlowdimlem16  27461  axcontlem10  27477  cusgrfilem1  27958  upgriswlk  28144  crctcshwlkn0  28322  wwlksnext  28394  wwlksnextwrd  28398  clwlkclwwlklem2a  28498  wwlksext2clwwlk  28557  grpoidinv  29006  grporcan  29016  grpoinvid1  29026  grpoinvid2  29027  grpolcan  29028  ablo4  29048  nvabs  29170  minvecolem7  29381  htthlem  29415  hvadd4  29534  hvaddsub4  29576  shscli  29815  pjspansn  30075  fh1  30116  fh2  30117  cm2j  30118  chscllem2  30136  spansncvi  30150  5oalem2  30153  5oalem5  30156  5oalem6  30157  3oalem2  30161  hoadd4  30282  cnvunop  30416  bralnfn  30446  eighmorth  30462  hmops  30518  hmopm  30519  adjlnop  30584  adjmul  30590  adjadd  30591  nmopcoi  30593  kbass5  30618  kbass6  30619  hstle  30728  stlesi  30739  mdsl0  30808  mdexchi  30833  atom1d  30851  superpos  30852  cvexchlem  30866  atomli  30880  atcvatlem  30883  chirredlem2  30889  chirredlem3  30890  atcvat4i  30895  mdsymlem1  30901  mdsymlem3  30903  mdsymlem5  30905  mdsymlem6  30906  sumdmdlem  30916  sumdmdlem2  30917  cdj1i  30931  opeldifid  31073  isoun  31169  1stpreimas  31173  f1od2  31191  ccatf1  31358  archirngz  31578  archiabllem1  31582  archiabllem2c  31584  rngurd  31617  qusxpid  31697  indf1ofs  32134  esum2d  32201  cntmeas  32334  ddemeas  32344  carsgclctunlem1  32424  itgeq12dv  32433  eulerpartlemgc  32469  eulerpartlemb  32475  eulerpartlemgs2  32487  ballotlemfc0  32599  ballotlemfcc  32600  reprss  32737  reprpmtf1o  32746  hgt750lemb  32776  bnj607  33035  derangenlem  33272  subfacp1lem3  33283  subfacp1lem5  33285  cvmliftmolem2  33383  cvmliftlem6  33391  cvmlift2lem5  33408  cvmlift2lem7  33410  cvmlift2lem9  33412  mppspstlem  33672  dfon2lem6  33895  sexp2  33923  noresle  33974  nosupno  33980  nosupbday  33982  noinfno  33995  bday1s  34099  colinbtwnle  34494  finminlem  34581  nn0prpwlem  34585  isfne  34602  neibastop1  34622  neibastop2lem  34623  neibastop3  34625  tailfb  34640  onsuct0  34704  nndivsub  34720  knoppcnlem6  34752  knoppndvlem9  34774  knoppndvlem18  34783  knoppndvlem21  34786  bj-prmoore  35358  bj-finsumval0  35528  rdgeqoa  35613  pibt2  35660  lindsadd  35842  matunitlindflem2  35846  poimirlem4  35853  poimirlem11  35860  poimirlem12  35861  poimirlem13  35862  poimirlem25  35874  poimirlem28  35877  heicant  35884  mblfinlem2  35887  mblfinlem3  35888  mblfinlem4  35889  mbfposadd  35896  itg2addnclem3  35902  ftc1anclem5  35926  ftc1anclem6  35927  ftc1anclem7  35928  ftc1anc  35930  frinfm  35965  filbcmb  35970  seqpo  35977  sstotbnd2  36004  isbndx  36012  ssbnd  36018  prdsbnd  36023  ismtycnv  36032  ismtyres  36038  heiborlem3  36043  heibor  36051  ghomdiv  36122  grpokerinj  36123  isdrngo2  36188  rngohomco  36204  rngoisocnv  36211  rngoisoco  36212  crngm4  36233  crngohomfo  36236  isidlc  36245  ispridl2  36268  ispridlc  36300  prtlem16  37103  ax12eq  37175  ax12el  37176  lshpcmp  37222  omllaw3  37479  omlfh1N  37492  cvratlem  37656  cvrat3  37677  cvrat4  37678  ps-2  37713  elpaddn0  38035  paddasslem10  38064  cdleme0cp  38449  cdleme32a  38676  cdlemeg49lebilem  38774  cdleme50eq  38776  tendoeq2  39009  diaglbN  39290  diameetN  39291  diainN  39292  dvhopN  39351  djaclN  39371  djajN  39372  dihopelvalcpre  39483  dih1dimatlem  39564  dihmeetcl  39580  djhcl  39635  mapdpglem2  39908  3factsumint1  40250  sticksstones22  40348  metakunt2  40350  isdomn4  40396  frlmsnic  40479  fsuppind  40495  mhphf  40501  0prjspn  40681  prjcrv0  40686  infdesc  40696  ismrc  40739  eldioph2  40800  lzenom  40808  rexrabdioph  40832  fphpdo  40855  irrapxlem3  40862  elpell14qr2  40900  pell14qrreccl  40902  pell14qrdich  40907  pellfundglb  40923  monotoddzzfi  40981  2nn0ind  40984  jm2.21  41033  jm2.22  41034  dnnumch3  41089  dnwech  41090  fnwe2lem2  41093  hbtlem6  41171  imo72b2lem1  42014  mnuprdlem1  42124  mnuprdlem2  42125  cncmpmax  42809  disjf1  42961  eliccelioc  43309  fprodexp  43385  fprodabs2  43386  mullimc  43407  mullimcf  43414  islpcn  43430  limsuppnfdlem  43492  liminfval2  43559  xlimmnfvlem1  43623  xlimmnfvlem2  43624  xlimpnfvlem1  43627  xlimpnfvlem2  43628  cncfshift  43665  cncfperiod  43670  fprodcncf  43691  dvnprodlem1  43737  dvnprodlem2  43738  stoweidlem34  43825  stoweidlem48  43839  stoweidlem60  43851  fourierdlem42  43940  fourierdlem60  43957  fourierdlem61  43958  fourierdlem63  43960  fourierdlem65  43962  fourierdlem87  43984  fourierdlem97  43994  elaa2  44025  etransclem46  44071  etransc  44074  salrestss  44150  sge0iunmptlemfi  44202  isomennd  44320  ovnsslelem  44349  ovolval4lem2  44439  smflimlem3  44562  smflimlem4  44563  smflimlem6  44565  smfpimbor1lem1  44587  smflimmpt  44599  smflimsupmpt  44618  smfliminfmpt  44621  fsetsnf1  44811  fcoresf1  44828  fvelsetpreimafv  45104  icceuelpart  45153  prproropf1olem4  45223  fmtnoprmfac2  45284  bgoldbtbndlem2  45523  bgoldbtbndlem3  45524  srhmsubc  45899  srhmsubcALTV  45917  catprs  46557  prsthinc  46600  aacllem  46770