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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  disjxiun  5146  frpomin  6342  fsnex  7281  f1prex  7282  isotr  7333  weniso  7351  riota5f  7394  frxp2  8130  frxp3  8137  xpord3pred  8138  poseq  8144  fprlem2  8286  tfrlem9a  8386  oaass  8561  oeeui  8602  oaabs2  8648  coflton  8670  cofon1  8671  naddssim  8684  resixpfo  8930  omxpenlem  9073  pw2f1olem  9076  fopwdom  9080  fofinf1o  9327  marypha1lem  9428  ordiso2  9510  oismo  9535  ixpiunwdom  9585  cantnf  9688  ttrclss  9715  fseqenlem1  10019  iunfictbso  10109  dfac12lem2  10139  dfac12lem3  10140  infunsdom1  10208  infpssrlem5  10302  fin23lem24  10317  isf32lem2  10349  isf32lem4  10351  isf34lem4  10372  fin1a2lem12  10406  fin1a2lem13  10407  ttukeylem6  10509  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  winalim2  10691  wunex2  10733  tskord  10775  prlem934  11028  mulcmpblnr  11066  dedekind  11377  addrid  11394  cnegex  11395  negeu  11450  add20  11726  divdivdiv  11915  ltmul12a  12070  lemul12a  12072  lediv12a  12107  supaddc  12181  supmul1  12183  cru  12204  uzwo3  12927  xleadd1a  13232  xmullem  13243  xmulgt0  13262  xlemul1a  13267  ixxun  13340  ixxss12  13344  ioodisj  13459  fz0fzelfz0  13607  mulexpz  14068  rpexpmord  14133  leexp1a  14140  expmulnbnd  14198  hashf1  14418  fi1uzind  14458  brfi1indALT  14461  swrdccat  14685  reuccatpfxs1  14697  abs3lem  15285  rexanre  15293  cau3lem  15301  limsupgre  15425  limsupbnd2  15427  o1lo1  15481  rlimclim1  15489  rlimclim  15490  rlimcn1  15532  rlimcn3  15534  o1of2  15557  o1rlimmul  15563  lo1add  15571  lo1mul  15572  isercolllem1  15611  climcau  15617  caucvgrlem  15619  caucvgb  15626  summolem2  15662  summo  15663  modfsummod  15740  o1fsum  15759  prodmolem2  15879  addmodlteqALT  16268  rpdvds  16597  isprm5  16644  isprm6  16651  pclem  16771  pcqmul  16786  pcexp  16792  pcneg  16807  pcprmpw2  16815  pcadd  16822  pcmpt  16825  4sqlem13  16890  vdwlem2  16915  vdwlem7  16920  vdwlem12  16925  ramval  16941  ramub2  16947  ramz2  16957  ramcl  16962  cshwshashlem2  17030  imasval  17457  imasdsval  17461  mreexexd  17592  acsfn  17603  issubc3  17799  idfucl  17831  funcres2c  17852  isnat  17898  fucpropd  17930  xpcval  18129  xpcco  18135  prfval  18151  evlf2  18171  evlfcl  18175  curf12  18180  curf1cl  18181  curf2  18182  curfcl  18185  curf2ndf  18200  hof2val  18209  hofcl  18212  hofpropd  18220  yonedalem4a  18228  yonedainv  18234  drsdirfi  18258  pospo  18298  poslubmo  18364  posglbmo  18365  isipodrs  18490  acsinfd  18509  gsumvalx  18595  gsumpropd2lem  18598  sgrppropd  18622  ismndd  18647  mndpropd  18650  mhmeql  18707  mndind  18709  frmdup3lem  18747  mhmmnd  18947  issubg4  19025  ssnmz  19046  conjnmzb  19127  f1otrspeq  19315  psgneu  19374  pgpfi  19473  sylow2blem3  19490  slwhash  19492  fislw  19493  sylow3lem2  19496  lsmdisj2  19550  pj1eu  19564  efgredlem  19615  frgpuplem  19640  gexex  19721  frgpnabl  19743  dprdfadd  19890  dpjidcl  19928  pgpfac1lem3  19947  pgpfaclem3  19953  ablfac2  19959  ablsimpgcygd  19976  ablsimpgfind  19980  ablsimpgprmd  19985  ringpropd  20102  imadrhmcl  20413  islmhm2  20649  lmhmpropd  20684  lbsextlem4  20774  prmirredlem  21042  psgndiflemA  21154  lsmcss  21245  uvcf1  21347  frlmsslsp  21351  frlmup1  21353  assapropd  21426  psrval  21468  evlslem1  21645  mamucl  21901  mamuass  21902  mamudi  21903  mamudir  21904  mamuvs1  21905  mamuvs2  21906  mamulid  21943  mamurid  21944  dmatsubcl  22000  dmatmulcl  22002  scmatscm  22015  marrepval  22064  marepveval  22070  mdetunilem7  22120  gsummatr01lem4  22160  cpmatmcllem  22220  mat2pmatf1  22231  mat2pmatlin  22237  decpmatmul  22274  pm2mpmhmlem2  22321  chpidmat  22349  pptbas  22511  toponmre  22597  restbas  22662  iscncl  22773  cnrest2  22790  cnpdis  22797  lmcnp  22808  dishaus  22886  cmpcovf  22895  tgcmp  22905  dfconn2  22923  clsconn  22934  2ndcctbss  22959  dis2ndc  22964  1stccnp  22966  islly2  22988  cldllycmp  22999  locfincmp  23030  comppfsc  23036  kgentopon  23042  txcls  23108  ptpjopn  23116  dfac14  23122  xkoccn  23123  txcnp  23124  txcmpb  23148  txlm  23152  xkopt  23159  xkoco1cn  23161  xkoco2cn  23162  qtopcn  23218  qtoprest  23221  regr1lem2  23244  xkocnv  23318  qtophmeo  23321  fmfnfmlem4  23461  hausflim  23485  hauspwpwf1  23491  fclscmp  23534  alexsublem  23548  alexsubALTlem2  23552  alexsubALTlem3  23553  ptcmplem3  23558  ptcmplem4  23559  ptcmplem5  23560  cnextfun  23568  tmdgsum2  23600  symgtgp  23610  tsmsval2  23634  tsmsgsum  23643  utoptop  23739  ismet2  23839  blin  23927  metss2lem  24020  methaus  24029  met1stc  24030  met2ndci  24031  prdsxmslem2  24038  metcnp3  24049  metcnpi3  24055  metustto  24062  metustfbas  24066  nlmvscn  24204  nrginvrcn  24209  xrsxmet  24325  reconnlem1  24342  reconn  24344  xrge0tsms  24350  xmetdcn2  24353  metdscn  24372  addcnlem  24380  fsumcn  24386  cnheiborlem  24470  cnheibor  24471  bndth  24474  lebnum  24480  nmoleub2lem2  24632  ipcn  24763  iscmet3  24810  caubl  24825  rrxdstprj1  24926  minveclem3b  24945  minveclem7  24952  pjthlem2  24955  pmltpc  24967  volfiniun  25064  ioombl1  25079  dyadss  25111  dyaddisjlem  25112  dyadmax  25115  dyadmbllem  25116  opnmbllem  25118  itg1addlem2  25214  itg10a  25228  mbfi1fseqlem6  25238  itg2seq  25260  itg2monolem1  25268  itg2gt0  25278  itgfsum  25344  limcfval  25389  ellimc2  25394  ellimc3  25396  limcres  25403  limciun  25411  dvres  25428  dveflem  25496  rolle  25507  dvlip2  25512  c1liplem1  25513  dvgt0lem1  25519  dvgt0  25521  dvlt0  25522  dvne0  25528  dvfsumrlimge0  25547  ftc1lem6  25558  itgsubst  25566  mdegmullem  25596  ply1domn  25641  ply1divex  25654  fta1g  25685  fta1b  25687  plyf  25712  dgrlem  25743  coeid  25752  plydivalg  25812  aannenlem1  25841  aalioulem3  25847  aalioulem6  25850  abelthlem8  25951  efif1olem4  26054  chordthm  26342  xrlimcnp  26473  jensen  26493  lgamcvglem  26544  lgamcvg2  26559  sqf11  26643  fsumvma2  26717  perfectlem2  26733  lgsdilem  26827  lgsquad2lem2  26888  lgsquad3  26890  2sqlem5  26925  2sqlem9  26930  2sqb  26935  rpvmasumlem  26990  dchrisum0flb  27013  dchrisum0  27023  pntpbnd  27091  pntibndlem3  27095  pntleml  27114  nolt02o  27198  nosupbday  27208  nosupbnd2  27219  noinfbday  27223  noinfbnd2  27234  noetasuplem4  27239  noetainflem4  27243  noetalem1  27244  conway  27300  slerec  27320  sltlpss  27401  addsprop  27460  tgjustc1  27726  tgjustc2  27727  legov  27836  legtrid  27842  tglinethru  27887  tglnpt2  27892  tglineintmo  27893  mirreu3  27905  perpcom  27964  colperpexlem3  27983  mideu  27989  opphllem1  27998  hlpasch  28007  lnopp2hpgb  28014  trgcopy  28055  brcgr  28158  brbtwn2  28163  colinearalg  28168  axsegcon  28185  axeuclidlem  28220  axcontlem9  28230  ecgrtg  28241  elntg  28242  eengtrkg  28244  upgr1eopALT  28377  usgredg4  28474  subuhgr  28543  subumgr  28545  usgr2wspthon  29219  clwlkclwwlkf1  29263  eupth2lems  29491  n4cyclfrgr  29544  vacn  29947  blocni  30058  ubthlem3  30125  minvecolem7  30136  chocunii  30554  pjhthmo  30555  pjhthlem2  30645  kbass5  31373  mdsymlem5  31660  foresf1o  31742  fcobij  31947  xrofsup  31980  mgcoval  32156  mgcf1o  32173  xrge0tsmsd  32209  symgcntz  32246  archirngz  32335  archiabllem2a  32340  isarchiofld  32435  prmidl2  32559  smatrcl  32776  reff  32819  ordtconnlem1  32904  qqhval2  32962  volmeas  33229  fiunelcarsg  33315  ballotlemfc0  33491  ballotlemfcc  33492  signstfvneq0  33583  derangenlem  34162  erdsze2lem1  34194  pconnconn  34222  connpconn  34226  cvxsconn  34234  cvmliftmolem2  34273  cvmliftmo  34275  cvmlift2lem10  34303  cvmlift2lem12  34305  cvmlift3lem7  34316  mrsubff1  34505  msubff1  34547  ifscgr  35016  cgrxfr  35027  btwnconn1lem13  35071  btwnconn1lem14  35072  outsideofeq  35102  ellines  35124  finminlem  35203  fnejoin2  35254  unbdqndv2  35387  irrdiff  36207  poimirlem13  36501  poimirlem14  36502  poimirlem32  36520  opnmbllem0  36524  mblfinlem3  36527  itg2addnclem  36539  itg2addnc  36542  ftc1cnnc  36560  upixp  36597  filbcmb  36608  sstotbnd2  36642  isbnd3  36652  prdsbnd2  36663  cntotbnd  36664  ismtyima  36671  bfp  36692  rrncmslem  36700  unichnidl  36899  lshpcmp  37858  islshpat  37887  lfl0f  37939  ishlat3N  38224  3dim1  38338  islvol5  38450  lvoli2  38452  lncvrelatN  38652  pclfinclN  38821  pexmidlem8N  38848  idltrn  39021  cdleme42keg  39357  cdleme42mgN  39359  cdlemf2  39433  cdlemg2cex  39462  trlcoat  39594  dihopelvalcpre  40119  dih1dimatlem  40200  dihjatcclem4  40292  lcfl7N  40372  lcfrlem9  40421  mapdh9a  40660  hdmapglem7  40800  aks4d1p8  40952  sticksstones11  40972  imacrhmcl  41089  fsuppind  41162  fsuppssind  41165  mhpind  41166  renegeulemv  41241  sn-subeu  41299  remulinvcom  41305  itrere  41339  retire  41340  prjspertr  41347  prjspreln0  41351  flt4lem7  41401  nna4b4nsq  41402  nacsfix  41450  mzpsubst  41486  mzpcompact2lem  41489  eldioph2lem2  41499  eldioph2  41500  eldioph2b  41501  diophin  41510  diophun  41511  irrapxlem3  41562  irrapxlem5  41564  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell14qrdich  41607  pell1qrge1  41608  pell1qrgaplem  41611  monotuz  41680  acongtr  41717  acongrep  41719  jm2.23  41735  jm2.26a  41739  jm2.26lem3  41740  jm2.26  41741  jm2.27  41747  wepwsolem  41784  fnwe2lem2  41793  kelac1  41805  kercvrlsm  41825  hbtlem5  41870  hbt  41872  mpaaeu  41892  cantnfresb  42074  onmcl  42081  tfsconcatun  42087  tfsconcatfn  42088  tfsconcatfv1  42089  tfsconcatfv2  42090  naddcnff  42112  rfovcnvf1od  42755  mnurndlem1  43040  cncmpmax  43716  rfcnnnub  43720  disjxp1  43756  iccintsng  44236  fprodcn  44316  lptioo2  44347  lptioo1  44348  limclner  44367  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem49  44765  stoweidlem59  44775  stoweidlem62  44778  fourierdlem60  44882  fourierdlem61  44883  fourierdlem87  44909  iundjiun  45176  ismeannd  45183  hoidmvle  45316  smfsuplem2  45528  2reu8i  45821  prproropf1olem2  46172  paireqne  46179  perfectALTVlem2  46390  mogoldbb  46453  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  isomgrtrlem  46506  mgmhmeql  46573  rngpropd  46673  mndpsuppss  47047  scmsuppss  47048  lindslinindsimp2lem5  47143  elfzolborelfzop1  47200  elbigolo1  47243  itschlc0xyqsol1  47452  itschlc0xyqsol  47453  iccdisj  47531  toslat  47607  functhinclem4  47664