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  5365  axprlem4OLD  5395  otsndisj  5496  otiunsndisj  5497  po2nr  5577  sotric  5593  sotrieq  5594  tz7.7  6383  fmptsnd  7167  fvtp1g  7196  f1cofveqaeqALT  7255  fsnex  7284  isocnv  7331  isores2  7334  isomin  7338  isoini  7339  f1oiso2  7353  ovmpodf  7569  offval  7687  ordsucun  7821  xp1st  8018  cnvf1olem  8107  fnse  8131  sexp2  8144  mpoxopoveq  8217  frrlem3  8287  frrlem13  8297  oalim  8519  omlim  8520  oaass  8548  omordi  8553  omwordri  8559  odi  8566  oen0  8574  oewordri  8580  nnawordi  8609  nnmordi  8619  omabs  8639  coflton  8659  nadd4  8687  erinxp  8791  dom2lem  8998  domssl  9004  mapen  9139  ssenen  9149  ssfiALT  9168  domfi  9183  php  9201  domunfican  9291  mapfien  9378  ordtypelem6  9495  ordtypelem7  9496  card2inf  9527  inf3lem6  9612  cantnfle  9650  cantnflem1b  9665  cantnflem1  9668  wemapwe  9676  ttrclselem2  9705  rankxplim3  9863  fseqenlem2  10028  dfac5lem4  10129  dfac2b  10133  cfsuc  10259  cfflb  10261  cofsmo  10271  infpssrlem4  10308  fin4en1  10311  ssfin4  10312  fin23lem26  10327  fin23lem22  10329  fin23lem27  10330  isf34lem4  10379  isf34lem5  10380  fin1a2lem12  10413  axdc3lem2  10453  axdc4lem  10457  ttukeylem6  10516  iundom2g  10548  pwcfsdom  10592  gchen2  10635  gchor  10636  fpwwe2lem6  10645  fpwwe2lem8  10647  fpwwe2lem10  10649  fpwwe2lem11  10650  fpwwe2  10652  pwfseqlem4  10671  gchina  10708  ltexprlem6  11050  prlem936  11056  mul4  11402  2addsub  11495  muladd  11670  ltleadd  11721  leord1  11765  eqord1  11766  ltord2  11767  leord2  11768  eqord2  11769  divmul3  11901  divcan7  11948  divadddiv  11954  lemul2a  12094  lemul12b  12096  ltmuldiv2  12113  ltdivmul  12114  ledivmul  12115  ltdivmul2  12116  lt2mul2div  12117  ledivmul2  12118  lemuldiv2  12120  lt2msq  12124  ltdiv23  12130  lediv23  12131  fimaxre  12183  supadd  12207  supmullem1  12209  cju  12238  zextlt  12695  suprzcl  12701  zmax  12994  xrlttr  13191  xrre3  13223  qbtwnre  13251  xrsupsslem  13359  xrinfmsslem  13360  supxrunb1  13371  supxrunb2  13372  ixxdisj  13413  iooshf  13479  icodisj  13529  iccf1o  13549  modid  13957  modadd1  13969  modmul1  13988  seqf1o  14107  expsub  14174  sqlecan  14273  bcval5  14382  hashmap  14500  hashfacen  14519  seqcoll  14529  ccatf1  14656  swrdswrdlem  14773  swrdccatin2  14798  cshwidxmod  14874  2cshwcshw  14896  cshwcshid  14898  resqreu  15339  lenegsq  15408  limsupbnd2  15570  icco1  15627  rlimresb  15652  rlimsqzlem  15736  rlimsqz  15737  rlimsqz2  15738  caucvgrlem  15760  fsum0diag2  15869  o1fsum  15900  ruclem8  16325  dvdsmulcr  16375  ndvdsadd  16500  bitsshft  16565  lcmdvds  16698  hashdvds  16866  eulerthlem2  16873  phisum  16882  pcqmul  16945  pcmpt  16984  prmreclem3  17010  4sqlem11  17047  0ram  17112  ramub1  17120  invfun  17853  initoeu2lem2  18104  coaval  18157  catcisolem  18199  funcestrcsetclem8  18235  fullestrcsetc  18239  embedsetcestrclem  18245  funcsetcestrclem8  18250  fullsetcestrc  18254  prfcl  18291  prf1st  18292  prf2nd  18293  1st2ndprf  18294  curfuncf  18326  isposd  18410  lubun  18603  isacs3lem  18630  pslem  18660  psss  18668  chnccat  18714  chnpof1  18718  pwsdiagmhm  18940  grpinvid1  19115  grpinvid2  19116  grplcan  19124  grpnpncan0  19159  dfgrp3lem  19161  dfgrp3  19162  grplactcnv  19166  0nsg  19292  eqger  19303  qusxpid  19308  eqg0subg  19324  qus0subgadd  19327  resghm  19359  conjghm  19376  subgga  19427  gaorber  19435  gastacl  19436  orbsta  19440  symgextf1lem  19547  psgnunilem2  19622  odid  19665  odmulg  19683  gexid  19708  odcau  19731  lsmssv  19770  lsmcom2  19782  pj1ghm  19830  frgpuptf  19897  frgpup1  19902  ghmplusg  19973  cyggex2  20024  gsumval3eu  20031  gsumval3  20034  ablfac1eu  20202  pgpfac1lem5  20208  ablsimpgfind  20239  ringurd  20324  srhmsubc  20842  isdomn4  20877  isdrngd  20931  isdrngdOLD  20933  issrngd  21021  lmhmf1o  21230  lmhmima  21231  lmhmpreima  21232  lspextmo  21240  pwssplit2  21244  pwssplit3  21245  lspdisj  21312  islbs3  21342  lbsextlem4  21348  drngnidl  21440  rngqiprngghmlem2  21491  rngqiprnglinlem1  21494  rngqiprngghm  21502  lidldvgen  21565  cnsubrg  21640  znunit  21776  cygznlem3  21782  dsmmsubg  21956  dsmmlss  21957  frlmsslsp  22009  frlmup1  22011  lindfrn  22034  f1lindf  22035  issubassa2  22107  psrbagconf1o  22144  psrgrp  22171  evlslem2  22295  mhplss  22383  psdmul  22394  psdmvr  22397  ply1sclf1  22515  mamuass  22624  dmatmul  22719  dmatsubcl  22720  dmatmulcl  22722  dmatcrng  22724  scmataddcl  22738  scmatsubcl  22739  scmatcrng  22743  mdetunilem2  22835  matunitlindflem2  22902  pm2mpf1  23024  pm2mpghm  23041  eltg2  23183  ntrss  23280  opncldf1  23309  ssnei2  23341  neindisj  23342  restopnb  23400  restntr  23407  tgcmp  23626  hauscmplem  23631  2ndc1stc  23676  2ndcdisj  23682  2ndcomap  23684  restlly  23709  lly1stc  23722  isref  23735  islocfin  23743  comppfsc  23758  txcls  23830  txdis1cn  23861  pthaus  23864  txlm  23874  qtoptop2  23925  qtopomap  23944  kqt0lem  23962  pt1hmeo  24032  ptuncnv  24033  xkocnv  24040  fbasfip  24094  fgabs  24105  fbasrn  24110  elfm2  24174  fmfnfmlem2  24181  fmfnfmlem4  24183  ptcmplem3  24280  ptcmplem4  24281  tsmsres  24370  tsmsxplem1  24379  utoptop  24460  elbl2ps  24615  elbl2  24616  blin  24647  xmeter  24659  xmetresbl  24663  stdbdxmet  24741  metrest  24750  metustexhalf  24782  dscmet  24798  nrmmetd  24800  tngngp2  24878  nmoi2  24956  icccmplem2  25050  reconnlem2  25054  metdstri  25078  metdsle  25079  metdsre  25080  metnrmlem3  25088  fsumcn  25098  icccvx  25178  bndth  25186  evth  25187  reparphti  25225  pi1blem  25267  tcphcph  25465  iscfil2  25494  cfilfcls  25502  iscau4  25507  iscauf  25508  caucfil  25511  cncmet  25550  minveclem7  25663  ovoliunlem1  25730  ovolicc2lem2  25746  ovolicc2lem3  25747  ovolicc2lem4  25748  ovolicc2lem5  25749  ovolicc2  25750  voliunlem3  25780  voliun  25782  ioombl  25793  volivth  25835  ismbfd  25867  ismbf3d  25882  itg1addlem1  25920  i1fadd  25923  itg1addlem4  25927  itg2split  25977  itg2monolem1  25978  itg2gt0  25988  ibllem  25992  itgvallem3  26013  iblposlem  26019  bddiblnc  26069  dvmptfsum  26202  rolle  26217  dvlip  26220  c1liplem1  26223  lhop1  26241  lhop2  26242  dvcvx  26247  dvfsumge  26249  dvfsumrlimge0  26257  dvfsumrlim  26258  dvfsum2  26261  mdegaddle  26299  mdegvscale  26300  mdegmullem  26303  ply1divex  26362  coeeulem  26450  plyco  26467  dgrlt  26492  vieta1  26544  ulmss  26633  ulmdvlem3  26638  iblulm  26643  tanord  26775  eff1olem  26785  logdivlt  26858  logccv  26900  lawcos  27053  xrlimcnp  27205  cxp2limlem  27212  cxp2lim  27213  cxploglim2  27215  divsqrtsumo1  27220  lgambdd  27273  sqff1o  27418  dvdsppwf1o  27422  dvdsflf1o  27423  musum  27427  muinv  27429  fsumdvdsmul  27431  sgmmul  27437  fsumvma  27449  logfac2  27453  chpchtsum  27455  logfacrlim  27460  logexprlim  27461  dchrelbas3  27474  dchrmulcl  27485  bposlem1  27520  lgsdchr  27591  lgsquadlem1  27616  lgsquadlem2  27617  lgsquad2lem2  27621  chebbnd1lem1  27705  chpchtlim  27715  rplogsumlem2  27721  dchrmusum2  27730  dchrvmasumlem1  27731  dchrvmasum2lem  27732  dchrvmasumlem2  27734  dchrvmasumlem3  27735  dchrvmasumiflem2  27738  dchrisum0flb  27746  dchrisum0fno1  27747  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  rplogsum  27763  mulogsum  27768  mulog2sumlem2  27771  vmalogdivsum2  27774  2vmadivsumlem  27776  selberglem2  27782  selberg3lem1  27793  selberg4lem1  27796  selberg4  27797  pntrsumo1  27801  selberg34r  27807  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntibndlem3  27828  pntlemp  27846  ostthlem1  27863  ostth3  27874  ltsres  27898  noresle  27933  nosupno  27939  nosupbday  27941  noinfno  27954  bday1  28079  cutlt  28197  addsproplem2  28235  negsproplem2  28294  mulsuniflem  28414  mulsunif2lem  28434  precsexlem9  28480  precsexlem10  28481  precsexlem11  28482  om2noseqlt  28564  om2noseqlt2  28565  om2noseqf1o  28566  om2noseqrdg  28569  noseqrdgfn  28571  bdaypw2n0bndlem  28728  bdayfinbndlem1  28732  recut  28759  elreno2  28760  renegscl  28763  ercgrg  28859  oppperpex  29108  axlowdimlem15  29413  axlowdimlem16  29414  axcontlem10  29430  cusgrfilem1  29915  upgriswlk  30100  crctcshwlkn0  30289  wwlksnext  30361  wwlksnextwrd  30365  clwlkclwwlklem2a  30468  wwlksext2clwwlk  30527  grpoidinv  30989  grporcan  30999  grpoinvid1  31009  grpoinvid2  31010  grpolcan  31011  ablo4  31031  nvabs  31153  minvecolem7  31364  htthlem  31398  hvadd4  31517  hvaddsub4  31559  shscli  31798  pjspansn  32058  fh1  32099  fh2  32100  cm2j  32101  chscllem2  32119  spansncvi  32133  5oalem2  32136  5oalem5  32139  5oalem6  32140  3oalem2  32144  hoadd4  32265  cnvunop  32399  bralnfn  32429  eighmorth  32445  hmops  32501  hmopm  32502  adjlnop  32567  adjmul  32573  adjadd  32574  nmopcoi  32576  kbass5  32601  kbass6  32602  hstle  32711  stlesi  32722  mdsl0  32791  mdexchi  32816  atom1d  32834  superpos  32835  cvexchlem  32849  atomli  32863  atcvatlem  32866  chirredlem2  32872  chirredlem3  32873  atcvat4i  32878  mdsymlem1  32884  mdsymlem3  32886  mdsymlem5  32888  mdsymlem6  32889  sumdmdlem  32899  sumdmdlem2  32900  cdj1i  32914  opeldifid  33072  isoun  33174  1stpreimas  33178  f1od2  33190  indf1ofs  33312  archirngz  33629  archiabllem1  33633  archiabllem2c  33635  esum2d  34603  cntmeas  34737  ddemeas  34747  carsgclctunlem1  34828  itgeq12dv  34837  eulerpartlemgc  34873  eulerpartlemb  34879  eulerpartlemgs2  34891  ballotlemfc0  35004  ballotlemfcc  35005  reprss  35125  reprpmtf1o  35134  hgt750lemb  35164  bnj607  35425  fissorduni  35594  derangenlem  35750  subfacp1lem3  35761  subfacp1lem5  35763  cvmliftmolem2  35861  cvmliftlem6  35869  cvmlift2lem5  35886  cvmlift2lem7  35888  cvmlift2lem9  35890  mppspstlem  36150  dfon2lem6  36365  colinbtwnle  36698  nmulrid  36777  ltnadd  36798  nadddilem2  36801  nadddilem4  36803  finminlem  36937  nn0prpwlem  36941  isfne  36958  neibastop1  36978  neibastop2lem  36979  neibastop3  36981  tailfb  36996  onsuct0  37060  nndivsub  37076  mh-inf3f1  37160  knoppcnlem6  37195  knoppndvlem9  37217  knoppndvlem18  37226  knoppndvlem21  37229  bj-prmoore  37865  bj-finsumval0  38037  rdgeqoa  38124  pibt2  38171  lindsadd  38367  poimirlem4  38373  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem25  38394  poimirlem28  38397  heicant  38404  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  mbfposadd  38416  itg2addnclem3  38422  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anc  38450  frinfm  38485  filbcmb  38490  seqpo  38497  sstotbnd2  38524  isbndx  38532  ssbnd  38538  prdsbnd  38543  ismtycnv  38552  ismtyres  38558  heiborlem3  38563  heibor  38571  ghomdiv  38642  grpokerinj  38643  isdrngo2  38708  rngohomco  38724  rngoisocnv  38731  rngoisoco  38732  crngm4  38753  crngohomfo  38756  isidlc  38765  ispridl2  38788  ispridlc  38820  prtlem16  39742  ax12eq  39814  ax12el  39815  lshpcmp  39861  omllaw3  40118  omlfh1N  40131  cvratlem  40294  cvrat3  40315  cvrat4  40316  ps-2  40351  elpaddn0  40673  paddasslem10  40702  cdleme0cp  41087  cdleme32a  41314  cdlemeg49lebilem  41412  cdleme50eq  41414  tendoeq2  41647  diaglbN  41928  diameetN  41929  diainN  41930  dvhopN  41989  djaclN  42009  djajN  42010  dihopelvalcpre  42121  dih1dimatlem  42202  dihmeetcl  42218  djhcl  42273  mapdpglem2  42546  3factsumint1  42887  sticksstones22  43034  unitscyglem4  43064  imacrhmcl  43402  frlmsnic  43422  psrmnd  43425  evlselvlem  43434  fsuppind  43436  0prjspn  43474  infdesc  43489  ismrc  43546  eldioph2  43607  lzenom  43615  rexrabdioph  43635  fphpdo  43658  irrapxlem3  43665  elpell14qr2  43703  pell14qrreccl  43705  pell14qrdich  43710  pellfundglb  43726  monotoddzzfi  43783  2nn0ind  43786  jm2.21  43835  jm2.22  43836  dnnumch3  43888  dnwech  43889  fnwe2lem2  43892  hbtlem6  43970  cantnfresb  44165  imo72b2lem1  45009  mnuprdlem1  45096  mnuprdlem2  45097  relpmin  45775  traxext  45800  cncmpmax  45866  disjf1  46015  eliccelioc  46351  fprodexp  46424  fprodabs2  46425  mullimc  46446  mullimcf  46453  islpcn  46467  limsuppnfdlem  46529  liminfval2  46596  xlimmnfvlem1  46660  xlimmnfvlem2  46661  xlimpnfvlem1  46664  xlimpnfvlem2  46665  cncfshift  46702  cncfperiod  46707  fprodcncf  46728  dvnprodlem1  46774  dvnprodlem2  46775  stoweidlem34  46862  stoweidlem48  46876  stoweidlem60  46888  fourierdlem42  46977  fourierdlem60  46994  fourierdlem61  46995  fourierdlem63  46997  fourierdlem65  46999  fourierdlem87  47021  fourierdlem97  47031  elaa2  47062  etransclem46  47108  etransc  47111  salrestss  47189  sge0iunmptlemfi  47241  isomennd  47359  ovnsslelem  47388  ovolval4lem2  47478  smflimlem3  47601  smflimlem4  47602  smflimlem6  47604  smfpimbor1lem1  47626  smflimmpt  47638  smflimsupmpt  47657  smfliminfmpt  47660  fsetsnf1  47940  fcoresf1  47957  fvelsetpreimafv  48287  icceuelpart  48336  prproropf1olem4  48406  fmtnoprmfac2  48470  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  gpg3nbgrvtx0ALT  48993  gpg3nbgrvtx1  48994  srhmsubcALTV  49240  xpco2  49785  catprs  49937  uppropd  50107  thincciso2  50381  prsthinc  50390  functermc  50434  fulltermc  50437  lmdran  50597  cmdlan  50598  aacllem  50772