Theorem simplrr 790

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 490	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 740	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:  disjxiun  5104  frpomin  6342  fsnex  7287  f1prex  7288  isotr  7340  weniso  7360  riota5f  7401  frxp2  8145  frxp3  8152  xpord3pred  8153  poseq  8159  fprlem2  8303  tfrlem9a  8378  oaass  8551  oeeui  8593  oaabs2  8640  coflton  8662  cofon1  8663  naddssim  8677  resixpfo  8946  omxpenlem  9079  pw2f1olem  9082  fopwdom  9086  fofinf1o  9302  marypha1lem  9406  ordiso2  9490  oismo  9515  ixpiunwdom  9565  cantnf  9675  ttrclss  9702  fseqenlem1  10030  iunfictbso  10120  dfac12lem2  10150  dfac12lem3  10151  infunsdom1  10217  infpssrlem5  10312  fin23lem24  10327  isf32lem2  10359  isf32lem4  10361  isf34lem4  10382  fin1a2lem12  10416  fin1a2lem13  10417  ttukeylem6  10519  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  winalim2  10708  wunex2  10750  tskord  10792  prlem934  11045  mulcmpblnr  11083  dedekind  11400  addrid  11417  cnegex  11418  negeu  11474  add20  11753  divdivdiv  11943  ltmul12a  12098  lemul12a  12100  lediv12a  12135  supaddc  12209  supmul1  12211  cru  12237  uzwo3  12995  xleadd1a  13307  xmullem  13318  xmulgt0  13337  xlemul1a  13342  ixxun  13416  ixxss12  13420  ioodisj  13537  fz0fzelfz0  13691  mulexpz  14168  rpexpmord  14234  leexp1a  14241  expmulnbnd  14301  hashf1  14524  fi1uzind  14574  brfi1indALT  14577  swrdccat  14806  reuccatpfxs1  14818  abs3lem  15428  rexanre  15436  cau3lem  15444  limsupgre  15570  limsupbnd2  15572  o1lo1  15626  rlimclim1  15634  rlimclim  15635  rlimcn1  15677  rlimcn3  15679  o1of2  15702  o1rlimmul  15708  lo1add  15716  lo1mul  15717  isercolllem1  15754  climcau  15760  caucvgrlem  15762  caucvgb  15769  summolem2  15804  summo  15805  modfsummod  15883  o1fsum  15902  prodmolem2  16026  addmodlteqALT  16419  rpdvds  16754  isprm5  16802  isprm6  16809  pclem  16934  pcqmul  16949  pcexp  16955  pcneg  16970  pcprmpw2  16978  pcadd  16985  pcmpt  16988  4sqlem13  17053  vdwlem2  17078  vdwlem7  17083  vdwlem12  17088  ramval  17104  ramub2  17110  ramz2  17120  ramcl  17125  cshwshashlem2  17192  imasval  17601  imasdsval  17605  mreexexd  17740  acsfn  17751  issubc3  17942  idfucl  17974  funcres2c  17996  isnat  18043  fucpropd  18073  xpcval  18269  xpcco  18275  prfval  18291  evlf2  18310  evlfcl  18314  curf12  18319  curf1cl  18320  curf2  18321  curfcl  18324  curf2ndf  18339  hof2val  18348  hofcl  18351  hofpropd  18359  yonedalem4a  18367  yonedainv  18373  drsdirfi  18397  pospo  18435  poslubmo  18501  posglbmo  18502  isipodrs  18629  acsinfd  18648  chnccat  18718  chnpof1  18722  gsumvalx  18780  gsumpropd2lem  18783  mgmhmeql  18820  sgrppropd  18835  ismndd  18861  mndpropd  18866  mndpsuppss  18874  mhmeql  18936  mndind  18938  frmdup3lem  18976  mhmmnd  19188  issubg4  19270  ssnmz  19290  conjnmzb  19381  f1otrspeq  19575  psgneu  19634  pgpfi  19733  sylow2blem3  19750  slwhash  19752  fislw  19753  sylow3lem2  19756  lsmdisj2  19810  pj1eu  19824  efgredlem  19875  frgpuplem  19900  gexex  19981  frgpnabl  20003  dprdfadd  20150  dpjidcl  20188  pgpfac1lem3  20207  pgpfaclem3  20213  ablfac2  20219  ablsimpgcygd  20236  ablsimpgfind  20240  ablsimpgprmd  20245  rngpropd  20310  ringpropd  20431  imadrhmcl  20964  islmhm2  21223  lmhmpropd  21258  lbsextlem4  21349  prmidl2  21530  prmirredlem  21686  psgndiflemA  21815  lsmcss  21906  uvcf1  22006  frlmsslsp  22010  frlmup1  22012  assapropd  22087  psrval  22131  evlslem1  22299  mamucl  22624  mamuass  22625  mamudi  22626  mamudir  22627  mamuvs1  22628  mamuvs2  22629  mamulid  22664  mamurid  22665  dmatsubcl  22721  dmatmulcl  22723  scmatscm  22736  marrepval  22785  marepveval  22791  mdetunilem7  22841  gsummatr01lem4  22881  cpmatmcllem  22944  mat2pmatf1  22955  mat2pmatlin  22961  decpmatmul  22998  pm2mpmhmlem2  23045  chpidmat  23073  pptbas  23234  toponmre  23319  restbas  23384  iscncl  23495  cnrest2  23512  cnpdis  23519  lmcnp  23530  dishaus  23608  cmpcovf  23617  tgcmp  23627  dfconn2  23645  clsconn  23656  2ndcctbss  23682  dis2ndc  23687  1stccnp  23689  islly2  23711  cldllycmp  23722  locfincmp  23753  comppfsc  23759  kgentopon  23765  txcls  23831  ptpjopn  23839  dfac14  23845  xkoccn  23846  txcnp  23847  txcmpb  23871  txlm  23875  xkopt  23882  xkoco1cn  23884  xkoco2cn  23885  qtopcn  23941  qtoprest  23944  regr1lem2  23967  xkocnv  24041  qtophmeo  24044  fmfnfmlem4  24184  hausflim  24208  hauspwpwf1  24214  fclscmp  24257  alexsublem  24271  alexsubALTlem2  24275  alexsubALTlem3  24276  ptcmplem3  24281  ptcmplem4  24282  ptcmplem5  24283  cnextfun  24291  tmdgsum2  24323  symgtgp  24333  tsmsval2  24357  tsmsgsum  24366  utoptop  24461  ismet2  24560  blin  24648  metss2lem  24738  methaus  24747  met1stc  24748  met2ndci  24749  prdsxmslem2  24756  metcnp3  24767  metcnpi3  24773  metustto  24780  metustfbas  24784  nlmvscn  24914  nrginvrcn  24919  xrsxmet  25037  reconnlem1  25054  reconn  25056  xrge0tsms  25062  xmetdcn2  25065  metdscn  25084  addcnlem  25092  fsumcn  25099  cnheiborlem  25183  cnheibor  25184  bndth  25187  lebnum  25193  nmoleub2lem2  25345  ipcn  25475  iscmet3  25522  caubl  25537  rrxdstprj1  25638  minveclem3b  25657  minveclem7  25664  pjthlem2  25667  pmltpc  25679  volfiniun  25776  ioombl1  25791  dyadss  25823  dyaddisjlem  25824  dyadmax  25827  dyadmbllem  25828  opnmbllem  25830  itg1addlem2  25926  itg10a  25939  mbfi1fseqlem6  25949  itg2seq  25971  itg2monolem1  25979  itg2gt0  25989  itgfsum  26056  limcfval  26101  ellimc2  26106  ellimc3  26108  limcres  26115  limciun  26123  dvres  26140  dveflem  26208  rolle  26219  dvlip2  26224  c1liplem1  26225  dvgt0lem1  26231  dvgt0  26233  dvlt0  26234  dvne0  26240  dvfsumrlimge0  26259  ftc1lem6  26270  itgsubst  26278  mdegmullem  26305  ply1domn  26351  ply1divex  26364  fta1g  26397  fta1b  26399  plyf  26425  dgrlem  26456  coeid  26465  plydivalg  26530  aannenlem1  26561  aalioulem3  26567  aalioulem6  26570  abelthlem8  26672  efif1olem4  26780  chordthm  27072  xrlimcnp  27203  jensen  27223  lgamcvglem  27274  lgamcvg2  27289  sqf11  27373  fsumvma2  27448  perfectlem2  27464  lgsdilem  27558  lgsquad2lem2  27619  lgsquad3  27621  2sqlem5  27656  2sqlem9  27661  2sqb  27666  rpvmasumlem  27721  dchrisum0flb  27744  dchrisum0  27754  pntpbnd  27822  pntibndlem3  27826  pntleml  27845  nolt02o  27929  nosupbday  27939  nosupbnd2  27950  noinfbday  27954  noinfbnd2  27965  noetasuplem4  27970  noetainflem4  27974  noetalem1  27975  conway  28042  lesrec  28062  ltslpss  28171  addsprop  28239  bdayons  28539  n0fincut  28618  eucliddivs  28639  remulscllem2  28764  tgjustc1  28814  tgjustc2  28815  legov  28925  legtrid  28931  tglinethru  28981  tglineintmo  28987  tglnpt2  28998  mirreu3  29003  perpcom  29065  colperpexlem3  29085  mideu  29091  opphllem1  29100  hlpasch  29111  lnopp2hpgb  29118  trgcopy  29188  brcgr  29343  brbtwn2  29348  colinearalg  29353  axsegcon  29370  axeuclidlem  29405  axcontlem9  29415  ecgrtg  29426  elntg  29427  eengtrkg  29429  upgr1eopALT  29560  usgredg4  29663  subuhgr  29732  subumgr  29734  usgr2wspthon  30422  clwlkclwwlkf1  30466  eupth2lems  30704  n4cyclfrgr  30757  vacn  31161  blocni  31272  ubthlem3  31339  minvecolem7  31350  chocunii  31768  pjhthmo  31769  pjhthlem2  31859  kbass5  32587  mdsymlem5  32874  foresf1o  32965  fcobij  33178  xrofsup  33225  mgcoval  33413  mgcf1o  33430  xrge0tsmsd  33500  symgcntz  33512  archirngz  33616  archiabllem2a  33621  isarchiofld  33626  mplvrpmmhm  34043  constrelextdg2  34244  smatrcl  34293  reff  34336  ordtconnlem1  34421  qqhval2  34479  volmeas  34729  fiunelcarsg  34814  ballotlemfc0  34991  ballotlemfcc  34992  signstfvneq0  35067  derangenlem  35737  erdsze2lem1  35769  pconnconn  35797  connpconn  35801  cvxsconn  35809  cvmliftmolem2  35848  cvmliftmo  35850  cvmlift2lem10  35878  cvmlift2lem12  35880  cvmlift3lem7  35891  mrsubff1  36080  msubff1  36122  r1peuqusdeg1  36209  ifscgr  36611  cgrxfr  36622  btwnconn1lem13  36666  btwnconn1lem14  36667  outsideofeq  36697  ellines  36719  nadddilem4  36790  finminlem  36924  fnejoin2  36975  weiunso  37072  unbdqndv2  37195  irrdiff  38065  qdiff  38066  poimirlem13  38369  poimirlem14  38370  poimirlem32  38388  opnmbllem0  38392  mblfinlem3  38395  itg2addnclem  38407  itg2addnc  38410  ftc1cnnc  38428  upixp  38466  filbcmb  38477  sstotbnd2  38511  isbnd3  38521  prdsbnd2  38532  cntotbnd  38533  ismtyima  38540  bfp  38561  rrncmslem  38569  unichnidl  38768  lshpcmp  39848  islshpat  39877  lfl0f  39929  ishlat3N  40214  3dim1  40327  islvol5  40439  lvoli2  40441  lncvrelatN  40641  pclfinclN  40810  pexmidlem8N  40837  idltrn  41010  cdleme42keg  41346  cdleme42mgN  41348  cdlemf2  41422  cdlemg2cex  41451  trlcoat  41583  dihopelvalcpre  42108  dih1dimatlem  42189  dihjatcclem4  42281  lcfl7N  42361  lcfrlem9  42410  mapdh9a  42649  hdmapglem7  42789  aks4d1p8  42940  isprimroot  42946  evl1gprodd  42970  sticksstones11  43009  grpods  43047  aks5lem8  43054  renegeulemv  43230  sn-subeu  43289  remulinvcom  43295  imacrhmcl  43389  fidomncyc  43404  fsuppind  43423  fsuppssind  43426  mhpind  43427  prjspertr  43438  prjspreln0  43442  flt4lem7  43492  nna4b4nsq  43493  nacsfix  43544  mzpsubst  43580  mzpcompact2lem  43583  eldioph2lem2  43593  eldioph2  43594  eldioph2b  43595  diophin  43604  diophun  43605  irrapxlem3  43652  irrapxlem5  43654  pell1234qrreccl  43682  pell1234qrmulcl  43683  pell14qrdich  43697  pell1qrge1  43698  pell1qrgaplem  43701  monotuz  43769  acongtr  43806  acongrep  43808  jm2.23  43824  jm2.26a  43828  jm2.26lem3  43829  jm2.26  43830  jm2.27  43836  wepwsolem  43870  fnwe2lem2  43879  kelac1  43891  kercvrlsm  43911  hbtlem5  43956  hbt  43958  mpaaeu  43978  cantnfresb  44152  onmcl  44159  tfsconcatun  44165  tfsconcatfn  44166  tfsconcatfv1  44167  tfsconcatfv2  44168  naddcnff  44190  rfovcnvf1od  44831  mnurndlem1  45092  cncmpmax  45853  rfcnnnub  45857  disjxp1  45890  iccintsng  46340  fprodcn  46417  lptioo2  46448  lptioo1  46449  limclner  46466  stoweidlem31  46846  stoweidlem34  46849  stoweidlem35  46850  stoweidlem49  46864  stoweidlem59  46874  stoweidlem62  46877  fourierdlem60  46981  fourierdlem61  46982  fourierdlem87  47008  iundjiun  47275  ismeannd  47282  hoidmvle  47415  smfsuplem2  47627  2reu8i  47988  prproropf1olem2  48391  paireqne  48398  nprmmul2  48415  perfectALTVlem2  48625  mogoldbb  48688  bgoldbtbndlem2  48709  bgoldbtbndlem3  48710  grimedg  48838  grlimprclnbgrvtx  48902  scmsuppss  49288  lindslinindsimp2lem5  49379  elfzolborelfzop1  49436  elbigolo1  49474  itschlc0xyqsol1  49683  itschlc0xyqsol  49684  iccdisj  49811  toslat  49895  iinfssclem3  49969  iinfssc  49970  iinfsubc  49971  imasubc3  50069  upciclem4  50082  uppropd  50094  natoppf  50142  tposcurf1  50212  fuco22  50252  fuco22natlem  50258  functhinclem4  50360  arweuthinc  50442