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  5089  frpomin  6288  fsnex  7220  f1prex  7221  isotr  7273  weniso  7291  riota5f  7334  frxp2  8077  frxp3  8084  xpord3pred  8085  poseq  8091  fprlem2  8234  tfrlem9a  8308  oaass  8479  oeeui  8520  oaabs2  8567  coflton  8589  cofon1  8590  naddssim  8603  resixpfo  8863  omxpenlem  8995  pw2f1olem  8998  fopwdom  9002  fofinf1o  9222  marypha1lem  9323  ordiso2  9407  oismo  9432  ixpiunwdom  9482  cantnf  9589  ttrclss  9616  fseqenlem1  9918  iunfictbso  10008  dfac12lem2  10039  dfac12lem3  10040  infunsdom1  10106  infpssrlem5  10201  fin23lem24  10216  isf32lem2  10248  isf32lem4  10250  isf34lem4  10271  fin1a2lem12  10305  fin1a2lem13  10306  ttukeylem6  10408  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  winalim2  10590  wunex2  10632  tskord  10674  prlem934  10927  mulcmpblnr  10965  dedekind  11279  addrid  11296  cnegex  11297  negeu  11353  add20  11632  divdivdiv  11825  ltmul12a  11980  lemul12a  11982  lediv12a  12018  supaddc  12092  supmul1  12094  cru  12120  uzwo3  12844  xleadd1a  13155  xmullem  13166  xmulgt0  13185  xlemul1a  13190  ixxun  13264  ixxss12  13268  ioodisj  13385  fz0fzelfz0  13537  mulexpz  14009  rpexpmord  14075  leexp1a  14082  expmulnbnd  14142  hashf1  14364  fi1uzind  14414  brfi1indALT  14417  swrdccat  14641  reuccatpfxs1  14653  abs3lem  15246  rexanre  15254  cau3lem  15262  limsupgre  15388  limsupbnd2  15390  o1lo1  15444  rlimclim1  15452  rlimclim  15453  rlimcn1  15495  rlimcn3  15497  o1of2  15520  o1rlimmul  15526  lo1add  15534  lo1mul  15535  isercolllem1  15572  climcau  15578  caucvgrlem  15580  caucvgb  15587  summolem2  15623  summo  15624  modfsummod  15701  o1fsum  15720  prodmolem2  15842  addmodlteqALT  16236  rpdvds  16571  isprm5  16618  isprm6  16625  pclem  16750  pcqmul  16765  pcexp  16771  pcneg  16786  pcprmpw2  16794  pcadd  16801  pcmpt  16804  4sqlem13  16869  vdwlem2  16894  vdwlem7  16899  vdwlem12  16904  ramval  16920  ramub2  16926  ramz2  16936  ramcl  16941  cshwshashlem2  17008  imasval  17415  imasdsval  17419  mreexexd  17554  acsfn  17565  issubc3  17756  idfucl  17788  funcres2c  17810  isnat  17857  fucpropd  17887  xpcval  18083  xpcco  18089  prfval  18105  evlf2  18124  evlfcl  18128  curf12  18133  curf1cl  18134  curf2  18135  curfcl  18138  curf2ndf  18153  hof2val  18162  hofcl  18165  hofpropd  18173  yonedalem4a  18181  yonedainv  18187  drsdirfi  18211  pospo  18249  poslubmo  18315  posglbmo  18316  isipodrs  18443  acsinfd  18462  gsumvalx  18550  gsumpropd2lem  18553  mgmhmeql  18590  sgrppropd  18605  ismndd  18630  mndpropd  18633  mndpsuppss  18639  mhmeql  18700  mndind  18702  frmdup3lem  18740  mhmmnd  18943  issubg4  19024  ssnmz  19045  conjnmzb  19132  f1otrspeq  19326  psgneu  19385  pgpfi  19484  sylow2blem3  19501  slwhash  19503  fislw  19504  sylow3lem2  19507  lsmdisj2  19561  pj1eu  19575  efgredlem  19626  frgpuplem  19651  gexex  19732  frgpnabl  19754  dprdfadd  19901  dpjidcl  19939  pgpfac1lem3  19958  pgpfaclem3  19964  ablfac2  19970  ablsimpgcygd  19987  ablsimpgfind  19991  ablsimpgprmd  19996  rngpropd  20059  ringpropd  20173  imadrhmcl  20682  islmhm2  20942  lmhmpropd  20977  lbsextlem4  21068  prmirredlem  21379  psgndiflemA  21508  lsmcss  21599  uvcf1  21699  frlmsslsp  21703  frlmup1  21705  assapropd  21779  psrval  21822  evlslem1  21987  mamucl  22286  mamuass  22287  mamudi  22288  mamudir  22289  mamuvs1  22290  mamuvs2  22291  mamulid  22326  mamurid  22327  dmatsubcl  22383  dmatmulcl  22385  scmatscm  22398  marrepval  22447  marepveval  22453  mdetunilem7  22503  gsummatr01lem4  22543  cpmatmcllem  22603  mat2pmatf1  22614  mat2pmatlin  22620  decpmatmul  22657  pm2mpmhmlem2  22704  chpidmat  22732  pptbas  22893  toponmre  22978  restbas  23043  iscncl  23154  cnrest2  23171  cnpdis  23178  lmcnp  23189  dishaus  23267  cmpcovf  23276  tgcmp  23286  dfconn2  23304  clsconn  23315  2ndcctbss  23340  dis2ndc  23345  1stccnp  23347  islly2  23369  cldllycmp  23380  locfincmp  23411  comppfsc  23417  kgentopon  23423  txcls  23489  ptpjopn  23497  dfac14  23503  xkoccn  23504  txcnp  23505  txcmpb  23529  txlm  23533  xkopt  23540  xkoco1cn  23542  xkoco2cn  23543  qtopcn  23599  qtoprest  23602  regr1lem2  23625  xkocnv  23699  qtophmeo  23702  fmfnfmlem4  23842  hausflim  23866  hauspwpwf1  23872  fclscmp  23915  alexsublem  23929  alexsubALTlem2  23933  alexsubALTlem3  23934  ptcmplem3  23939  ptcmplem4  23940  ptcmplem5  23941  cnextfun  23949  tmdgsum2  23981  symgtgp  23991  tsmsval2  24015  tsmsgsum  24024  utoptop  24120  ismet2  24219  blin  24307  metss2lem  24397  methaus  24406  met1stc  24407  met2ndci  24408  prdsxmslem2  24415  metcnp3  24426  metcnpi3  24432  metustto  24439  metustfbas  24443  nlmvscn  24573  nrginvrcn  24578  xrsxmet  24696  reconnlem1  24713  reconn  24715  xrge0tsms  24721  xmetdcn2  24724  metdscn  24743  addcnlem  24751  fsumcn  24759  cnheiborlem  24851  cnheibor  24852  bndth  24855  lebnum  24861  nmoleub2lem2  25014  ipcn  25144  iscmet3  25191  caubl  25206  rrxdstprj1  25307  minveclem3b  25326  minveclem7  25333  pjthlem2  25336  pmltpc  25349  volfiniun  25446  ioombl1  25461  dyadss  25493  dyaddisjlem  25494  dyadmax  25497  dyadmbllem  25498  opnmbllem  25500  itg1addlem2  25596  itg10a  25609  mbfi1fseqlem6  25619  itg2seq  25641  itg2monolem1  25649  itg2gt0  25659  itgfsum  25726  limcfval  25771  ellimc2  25776  ellimc3  25778  limcres  25785  limciun  25793  dvres  25810  dveflem  25881  rolle  25892  dvlip2  25898  c1liplem1  25899  dvgt0lem1  25905  dvgt0  25907  dvlt0  25908  dvne0  25914  dvfsumrlimge0  25935  ftc1lem6  25946  itgsubst  25954  mdegmullem  25981  ply1domn  26027  ply1divex  26040  fta1g  26073  fta1b  26075  plyf  26101  dgrlem  26132  coeid  26141  plydivalg  26205  aannenlem1  26234  aalioulem3  26240  aalioulem6  26243  abelthlem8  26347  efif1olem4  26452  chordthm  26745  xrlimcnp  26876  jensen  26897  lgamcvglem  26948  lgamcvg2  26963  sqf11  27047  fsumvma2  27123  perfectlem2  27139  lgsdilem  27233  lgsquad2lem2  27294  lgsquad3  27296  2sqlem5  27331  2sqlem9  27336  2sqb  27341  rpvmasumlem  27396  dchrisum0flb  27419  dchrisum0  27429  pntpbnd  27497  pntibndlem3  27501  pntleml  27520  nolt02o  27605  nosupbday  27615  nosupbnd2  27626  noinfbday  27630  noinfbnd2  27641  noetasuplem4  27646  noetainflem4  27650  noetalem1  27651  conway  27710  slerec  27730  sltlpss  27822  addsprop  27888  bdayon  28178  n0sfincut  28251  eucliddivs  28270  remulscllem2  28370  tgjustc1  28420  tgjustc2  28421  legov  28530  legtrid  28536  tglinethru  28581  tglnpt2  28586  tglineintmo  28587  mirreu3  28599  perpcom  28658  colperpexlem3  28677  mideu  28683  opphllem1  28692  hlpasch  28701  lnopp2hpgb  28708  trgcopy  28749  brcgr  28845  brbtwn2  28850  colinearalg  28855  axsegcon  28872  axeuclidlem  28907  axcontlem9  28917  ecgrtg  28928  elntg  28929  eengtrkg  28931  upgr1eopALT  29062  usgredg4  29162  subuhgr  29231  subumgr  29233  usgr2wspthon  29910  clwlkclwwlkf1  29954  eupth2lems  30182  n4cyclfrgr  30235  vacn  30638  blocni  30749  ubthlem3  30816  minvecolem7  30827  chocunii  31245  pjhthmo  31246  pjhthlem2  31336  kbass5  32064  mdsymlem5  32351  foresf1o  32448  fcobij  32664  xrofsup  32710  mgcoval  32928  mgcf1o  32945  xrge0tsmsd  33015  symgcntz  33027  archirngz  33131  archiabllem2a  33136  isarchiofld  33141  prmidl2  33378  constrelextdg2  33714  smatrcl  33763  reff  33806  ordtconnlem1  33891  qqhval2  33949  volmeas  34198  fiunelcarsg  34284  ballotlemfc0  34461  ballotlemfcc  34462  signstfvneq0  34540  derangenlem  35144  erdsze2lem1  35176  pconnconn  35204  connpconn  35208  cvxsconn  35216  cvmliftmolem2  35255  cvmliftmo  35257  cvmlift2lem10  35285  cvmlift2lem12  35287  cvmlift3lem7  35298  mrsubff1  35487  msubff1  35529  r1peuqusdeg1  35616  ifscgr  36018  cgrxfr  36029  btwnconn1lem13  36073  btwnconn1lem14  36074  outsideofeq  36104  ellines  36126  finminlem  36292  fnejoin2  36343  weiunso  36440  unbdqndv2  36485  irrdiff  37300  poimirlem13  37613  poimirlem14  37614  poimirlem32  37632  opnmbllem0  37636  mblfinlem3  37639  itg2addnclem  37651  itg2addnc  37654  ftc1cnnc  37672  upixp  37709  filbcmb  37720  sstotbnd2  37754  isbnd3  37764  prdsbnd2  37775  cntotbnd  37776  ismtyima  37783  bfp  37804  rrncmslem  37812  unichnidl  38011  lshpcmp  38967  islshpat  38996  lfl0f  39048  ishlat3N  39333  3dim1  39446  islvol5  39558  lvoli2  39560  lncvrelatN  39760  pclfinclN  39929  pexmidlem8N  39956  idltrn  40129  cdleme42keg  40465  cdleme42mgN  40467  cdlemf2  40541  cdlemg2cex  40570  trlcoat  40702  dihopelvalcpre  41227  dih1dimatlem  41308  dihjatcclem4  41400  lcfl7N  41480  lcfrlem9  41529  mapdh9a  41768  hdmapglem7  41908  aks4d1p8  42060  isprimroot  42066  evl1gprodd  42090  sticksstones11  42129  grpods  42167  aks5lem8  42174  renegeulemv  42341  sn-subeu  42400  remulinvcom  42406  imacrhmcl  42487  fidomncyc  42508  fsuppind  42563  fsuppssind  42566  mhpind  42567  prjspertr  42578  prjspreln0  42582  flt4lem7  42632  nna4b4nsq  42633  nacsfix  42685  mzpsubst  42721  mzpcompact2lem  42724  eldioph2lem2  42734  eldioph2  42735  eldioph2b  42736  diophin  42745  diophun  42746  irrapxlem3  42797  irrapxlem5  42799  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell14qrdich  42842  pell1qrge1  42843  pell1qrgaplem  42846  monotuz  42914  acongtr  42951  acongrep  42953  jm2.23  42969  jm2.26a  42973  jm2.26lem3  42974  jm2.26  42975  jm2.27  42981  wepwsolem  43015  fnwe2lem2  43024  kelac1  43036  kercvrlsm  43056  hbtlem5  43101  hbt  43103  mpaaeu  43123  cantnfresb  43297  onmcl  43304  tfsconcatun  43310  tfsconcatfn  43311  tfsconcatfv1  43312  tfsconcatfv2  43313  naddcnff  43335  rfovcnvf1od  43977  mnurndlem1  44254  cncmpmax  45010  rfcnnnub  45014  disjxp1  45047  iccintsng  45504  fprodcn  45581  lptioo2  45612  lptioo1  45613  limclner  45632  stoweidlem31  46012  stoweidlem34  46015  stoweidlem35  46016  stoweidlem49  46030  stoweidlem59  46040  stoweidlem62  46043  fourierdlem60  46147  fourierdlem61  46148  fourierdlem87  46174  iundjiun  46441  ismeannd  46448  hoidmvle  46581  smfsuplem2  46793  2reu8i  47097  prproropf1olem2  47488  paireqne  47495  perfectALTVlem2  47706  mogoldbb  47769  bgoldbtbndlem2  47790  bgoldbtbndlem3  47791  grimedg  47919  grlimprclnbgrvtx  47983  scmsuppss  48355  lindslinindsimp2lem5  48447  elfzolborelfzop1  48504  elbigolo1  48542  itschlc0xyqsol1  48751  itschlc0xyqsol  48752  iccdisj  48882  toslat  48966  iinfssclem3  49041  iinfssc  49042  iinfsubc  49043  imasubc3  49141  upciclem4  49154  uppropd  49166  natoppf  49214  tposcurf1  49284  fuco22  49324  fuco22natlem  49330  functhinclem4  49432  arweuthinc  49514