Theorem simplrr 777

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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 727	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5090  frpomin  6293  fsnex  7223  f1prex  7224  isotr  7276  weniso  7294  riota5f  7337  frxp2  8080  frxp3  8087  xpord3pred  8088  poseq  8094  fprlem2  8237  tfrlem9a  8311  oaass  8482  oeeui  8523  oaabs2  8570  coflton  8592  cofon1  8593  naddssim  8606  resixpfo  8866  omxpenlem  8997  pw2f1olem  9000  fopwdom  9004  fofinf1o  9222  marypha1lem  9323  ordiso2  9407  oismo  9432  ixpiunwdom  9482  cantnf  9589  ttrclss  9616  fseqenlem1  9921  iunfictbso  10011  dfac12lem2  10042  dfac12lem3  10043  infunsdom1  10109  infpssrlem5  10204  fin23lem24  10219  isf32lem2  10251  isf32lem4  10253  isf34lem4  10274  fin1a2lem12  10308  fin1a2lem13  10309  ttukeylem6  10411  fpwwe2lem11  10538  fpwwe2lem12  10539  fpwwe2  10540  winalim2  10593  wunex2  10635  tskord  10677  prlem934  10930  mulcmpblnr  10968  dedekind  11282  addrid  11299  cnegex  11300  negeu  11356  add20  11635  divdivdiv  11828  ltmul12a  11983  lemul12a  11985  lediv12a  12021  supaddc  12095  supmul1  12097  cru  12123  uzwo3  12847  xleadd1a  13158  xmullem  13169  xmulgt0  13188  xlemul1a  13193  ixxun  13267  ixxss12  13271  ioodisj  13388  fz0fzelfz0  13540  mulexpz  14015  rpexpmord  14081  leexp1a  14088  expmulnbnd  14148  hashf1  14370  fi1uzind  14420  brfi1indALT  14423  swrdccat  14648  reuccatpfxs1  14660  abs3lem  15252  rexanre  15260  cau3lem  15268  limsupgre  15394  limsupbnd2  15396  o1lo1  15450  rlimclim1  15458  rlimclim  15459  rlimcn1  15501  rlimcn3  15503  o1of2  15526  o1rlimmul  15532  lo1add  15540  lo1mul  15541  isercolllem1  15578  climcau  15584  caucvgrlem  15586  caucvgb  15593  summolem2  15629  summo  15630  modfsummod  15707  o1fsum  15726  prodmolem2  15848  addmodlteqALT  16242  rpdvds  16577  isprm5  16624  isprm6  16631  pclem  16756  pcqmul  16771  pcexp  16777  pcneg  16792  pcprmpw2  16800  pcadd  16807  pcmpt  16810  4sqlem13  16875  vdwlem2  16900  vdwlem7  16905  vdwlem12  16910  ramval  16926  ramub2  16932  ramz2  16942  ramcl  16947  cshwshashlem2  17014  imasval  17421  imasdsval  17425  mreexexd  17560  acsfn  17571  issubc3  17762  idfucl  17794  funcres2c  17816  isnat  17863  fucpropd  17893  xpcval  18089  xpcco  18095  prfval  18111  evlf2  18130  evlfcl  18134  curf12  18139  curf1cl  18140  curf2  18141  curfcl  18144  curf2ndf  18159  hof2val  18168  hofcl  18171  hofpropd  18179  yonedalem4a  18187  yonedainv  18193  drsdirfi  18217  pospo  18255  poslubmo  18321  posglbmo  18322  isipodrs  18449  acsinfd  18468  chnccat  18538  chnpof1  18542  gsumvalx  18590  gsumpropd2lem  18593  mgmhmeql  18630  sgrppropd  18645  ismndd  18670  mndpropd  18673  mndpsuppss  18679  mhmeql  18740  mndind  18742  frmdup3lem  18780  mhmmnd  18983  issubg4  19064  ssnmz  19084  conjnmzb  19171  f1otrspeq  19365  psgneu  19424  pgpfi  19523  sylow2blem3  19540  slwhash  19542  fislw  19543  sylow3lem2  19546  lsmdisj2  19600  pj1eu  19614  efgredlem  19665  frgpuplem  19690  gexex  19771  frgpnabl  19793  dprdfadd  19940  dpjidcl  19978  pgpfac1lem3  19997  pgpfaclem3  20003  ablfac2  20009  ablsimpgcygd  20026  ablsimpgfind  20030  ablsimpgprmd  20035  rngpropd  20098  ringpropd  20212  imadrhmcl  20718  islmhm2  20978  lmhmpropd  21013  lbsextlem4  21104  prmirredlem  21415  psgndiflemA  21544  lsmcss  21635  uvcf1  21735  frlmsslsp  21739  frlmup1  21741  assapropd  21815  psrval  21858  evlslem1  22023  mamucl  22322  mamuass  22323  mamudi  22324  mamudir  22325  mamuvs1  22326  mamuvs2  22327  mamulid  22362  mamurid  22363  dmatsubcl  22419  dmatmulcl  22421  scmatscm  22434  marrepval  22483  marepveval  22489  mdetunilem7  22539  gsummatr01lem4  22579  cpmatmcllem  22639  mat2pmatf1  22650  mat2pmatlin  22656  decpmatmul  22693  pm2mpmhmlem2  22740  chpidmat  22768  pptbas  22929  toponmre  23014  restbas  23079  iscncl  23190  cnrest2  23207  cnpdis  23214  lmcnp  23225  dishaus  23303  cmpcovf  23312  tgcmp  23322  dfconn2  23340  clsconn  23351  2ndcctbss  23376  dis2ndc  23381  1stccnp  23383  islly2  23405  cldllycmp  23416  locfincmp  23447  comppfsc  23453  kgentopon  23459  txcls  23525  ptpjopn  23533  dfac14  23539  xkoccn  23540  txcnp  23541  txcmpb  23565  txlm  23569  xkopt  23576  xkoco1cn  23578  xkoco2cn  23579  qtopcn  23635  qtoprest  23638  regr1lem2  23661  xkocnv  23735  qtophmeo  23738  fmfnfmlem4  23878  hausflim  23902  hauspwpwf1  23908  fclscmp  23951  alexsublem  23965  alexsubALTlem2  23969  alexsubALTlem3  23970  ptcmplem3  23975  ptcmplem4  23976  ptcmplem5  23977  cnextfun  23985  tmdgsum2  24017  symgtgp  24027  tsmsval2  24051  tsmsgsum  24060  utoptop  24155  ismet2  24254  blin  24342  metss2lem  24432  methaus  24441  met1stc  24442  met2ndci  24443  prdsxmslem2  24450  metcnp3  24461  metcnpi3  24467  metustto  24474  metustfbas  24478  nlmvscn  24608  nrginvrcn  24613  xrsxmet  24731  reconnlem1  24748  reconn  24750  xrge0tsms  24756  xmetdcn2  24759  metdscn  24778  addcnlem  24786  fsumcn  24794  cnheiborlem  24886  cnheibor  24887  bndth  24890  lebnum  24896  nmoleub2lem2  25049  ipcn  25179  iscmet3  25226  caubl  25241  rrxdstprj1  25342  minveclem3b  25361  minveclem7  25368  pjthlem2  25371  pmltpc  25384  volfiniun  25481  ioombl1  25496  dyadss  25528  dyaddisjlem  25529  dyadmax  25532  dyadmbllem  25533  opnmbllem  25535  itg1addlem2  25631  itg10a  25644  mbfi1fseqlem6  25654  itg2seq  25676  itg2monolem1  25684  itg2gt0  25694  itgfsum  25761  limcfval  25806  ellimc2  25811  ellimc3  25813  limcres  25820  limciun  25828  dvres  25845  dveflem  25916  rolle  25927  dvlip2  25933  c1liplem1  25934  dvgt0lem1  25940  dvgt0  25942  dvlt0  25943  dvne0  25949  dvfsumrlimge0  25970  ftc1lem6  25981  itgsubst  25989  mdegmullem  26016  ply1domn  26062  ply1divex  26075  fta1g  26108  fta1b  26110  plyf  26136  dgrlem  26167  coeid  26176  plydivalg  26240  aannenlem1  26269  aalioulem3  26275  aalioulem6  26278  abelthlem8  26382  efif1olem4  26487  chordthm  26780  xrlimcnp  26911  jensen  26932  lgamcvglem  26983  lgamcvg2  26998  sqf11  27082  fsumvma2  27158  perfectlem2  27174  lgsdilem  27268  lgsquad2lem2  27329  lgsquad3  27331  2sqlem5  27366  2sqlem9  27371  2sqb  27376  rpvmasumlem  27431  dchrisum0flb  27454  dchrisum0  27464  pntpbnd  27532  pntibndlem3  27536  pntleml  27555  nolt02o  27640  nosupbday  27650  nosupbnd2  27661  noinfbday  27665  noinfbnd2  27676  noetasuplem4  27681  noetainflem4  27685  noetalem1  27686  conway  27746  slerec  27766  sltlpss  27859  addsprop  27925  bdayon  28215  n0sfincut  28288  eucliddivs  28307  remulscllem2  28409  tgjustc1  28459  tgjustc2  28460  legov  28569  legtrid  28575  tglinethru  28620  tglnpt2  28625  tglineintmo  28626  mirreu3  28638  perpcom  28697  colperpexlem3  28716  mideu  28722  opphllem1  28731  hlpasch  28740  lnopp2hpgb  28747  trgcopy  28788  brcgr  28885  brbtwn2  28890  colinearalg  28895  axsegcon  28912  axeuclidlem  28947  axcontlem9  28957  ecgrtg  28968  elntg  28969  eengtrkg  28971  upgr1eopALT  29102  usgredg4  29202  subuhgr  29271  subumgr  29273  usgr2wspthon  29953  clwlkclwwlkf1  29997  eupth2lems  30225  n4cyclfrgr  30278  vacn  30681  blocni  30792  ubthlem3  30859  minvecolem7  30870  chocunii  31288  pjhthmo  31289  pjhthlem2  31379  kbass5  32107  mdsymlem5  32394  foresf1o  32491  fcobij  32710  xrofsup  32757  mgcoval  32974  mgcf1o  32991  xrge0tsmsd  33049  symgcntz  33061  archirngz  33165  archiabllem2a  33170  isarchiofld  33175  prmidl2  33413  mplvrpmmhm  33583  constrelextdg2  33767  smatrcl  33816  reff  33859  ordtconnlem1  33944  qqhval2  34002  volmeas  34251  fiunelcarsg  34336  ballotlemfc0  34513  ballotlemfcc  34514  signstfvneq0  34592  derangenlem  35222  erdsze2lem1  35254  pconnconn  35282  connpconn  35286  cvxsconn  35294  cvmliftmolem2  35333  cvmliftmo  35335  cvmlift2lem10  35363  cvmlift2lem12  35365  cvmlift3lem7  35376  mrsubff1  35565  msubff1  35607  r1peuqusdeg1  35694  ifscgr  36095  cgrxfr  36106  btwnconn1lem13  36150  btwnconn1lem14  36151  outsideofeq  36181  ellines  36203  finminlem  36369  fnejoin2  36420  weiunso  36517  unbdqndv2  36562  irrdiff  37377  poimirlem13  37679  poimirlem14  37680  poimirlem32  37698  opnmbllem0  37702  mblfinlem3  37705  itg2addnclem  37717  itg2addnc  37720  ftc1cnnc  37738  upixp  37775  filbcmb  37786  sstotbnd2  37820  isbnd3  37830  prdsbnd2  37841  cntotbnd  37842  ismtyima  37849  bfp  37870  rrncmslem  37878  unichnidl  38077  lshpcmp  39093  islshpat  39122  lfl0f  39174  ishlat3N  39459  3dim1  39572  islvol5  39684  lvoli2  39686  lncvrelatN  39886  pclfinclN  40055  pexmidlem8N  40082  idltrn  40255  cdleme42keg  40591  cdleme42mgN  40593  cdlemf2  40667  cdlemg2cex  40696  trlcoat  40828  dihopelvalcpre  41353  dih1dimatlem  41434  dihjatcclem4  41526  lcfl7N  41606  lcfrlem9  41655  mapdh9a  41894  hdmapglem7  42034  aks4d1p8  42186  isprimroot  42192  evl1gprodd  42216  sticksstones11  42255  grpods  42293  aks5lem8  42300  renegeulemv  42467  sn-subeu  42526  remulinvcom  42532  imacrhmcl  42613  fidomncyc  42634  fsuppind  42689  fsuppssind  42692  mhpind  42693  prjspertr  42704  prjspreln0  42708  flt4lem7  42758  nna4b4nsq  42759  nacsfix  42810  mzpsubst  42846  mzpcompact2lem  42849  eldioph2lem2  42859  eldioph2  42860  eldioph2b  42861  diophin  42870  diophun  42871  irrapxlem3  42922  irrapxlem5  42924  pell1234qrreccl  42952  pell1234qrmulcl  42953  pell14qrdich  42967  pell1qrge1  42968  pell1qrgaplem  42971  monotuz  43039  acongtr  43076  acongrep  43078  jm2.23  43094  jm2.26a  43098  jm2.26lem3  43099  jm2.26  43100  jm2.27  43106  wepwsolem  43140  fnwe2lem2  43149  kelac1  43161  kercvrlsm  43181  hbtlem5  43226  hbt  43228  mpaaeu  43248  cantnfresb  43422  onmcl  43429  tfsconcatun  43435  tfsconcatfn  43436  tfsconcatfv1  43437  tfsconcatfv2  43438  naddcnff  43460  rfovcnvf1od  44102  mnurndlem1  44379  cncmpmax  45134  rfcnnnub  45138  disjxp1  45171  iccintsng  45628  fprodcn  45705  lptioo2  45736  lptioo1  45737  limclner  45754  stoweidlem31  46134  stoweidlem34  46137  stoweidlem35  46138  stoweidlem49  46152  stoweidlem59  46162  stoweidlem62  46165  fourierdlem60  46269  fourierdlem61  46270  fourierdlem87  46296  iundjiun  46563  ismeannd  46570  hoidmvle  46703  smfsuplem2  46915  2reu8i  47218  prproropf1olem2  47609  paireqne  47616  perfectALTVlem2  47827  mogoldbb  47890  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  grimedg  48040  grlimprclnbgrvtx  48104  scmsuppss  48476  lindslinindsimp2lem5  48568  elfzolborelfzop1  48625  elbigolo1  48663  itschlc0xyqsol1  48872  itschlc0xyqsol  48873  iccdisj  49003  toslat  49087  iinfssclem3  49162  iinfssc  49163  iinfsubc  49164  imasubc3  49262  upciclem4  49275  uppropd  49287  natoppf  49335  tposcurf1  49405  fuco22  49445  fuco22natlem  49451  functhinclem4  49553  arweuthinc  49635