Theorem simplrr 785

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5087  frpomin  6312  fsnex  7252  f1prex  7253  isotr  7305  weniso  7323  riota5f  7366  frxp2  8108  frxp3  8115  xpord3pred  8116  poseq  8122  fprlem2  8266  tfrlem9a  8341  oaass  8514  oeeui  8556  oaabs2  8603  coflton  8625  cofon1  8626  naddssim  8640  resixpfo  8903  omxpenlem  9035  pw2f1olem  9038  fopwdom  9042  fofinf1o  9261  marypha1lem  9365  ordiso2  9449  oismo  9474  ixpiunwdom  9524  cantnf  9634  ttrclss  9661  fseqenlem1  9966  iunfictbso  10056  dfac12lem2  10087  dfac12lem3  10088  infunsdom1  10154  infpssrlem5  10250  fin23lem24  10265  isf32lem2  10297  isf32lem4  10299  isf34lem4  10320  fin1a2lem12  10354  fin1a2lem13  10355  ttukeylem6  10457  fpwwe2lem11  10585  fpwwe2lem12  10586  fpwwe2  10587  winalim2  10640  wunex2  10682  tskord  10724  prlem934  10977  mulcmpblnr  11015  dedekind  11332  addrid  11349  cnegex  11350  negeu  11406  add20  11685  divdivdiv  11878  ltmul12a  12033  lemul12a  12035  lediv12a  12071  supaddc  12145  supmul1  12147  cru  12173  uzwo3  12930  xleadd1a  13242  xmullem  13253  xmulgt0  13272  xlemul1a  13277  ixxun  13351  ixxss12  13355  ioodisj  13472  fz0fzelfz0  13625  mulexpz  14101  rpexpmord  14167  leexp1a  14174  expmulnbnd  14234  hashf1  14456  fi1uzind  14506  brfi1indALT  14509  swrdccat  14734  reuccatpfxs1  14746  abs3lem  15338  rexanre  15346  cau3lem  15354  limsupgre  15480  limsupbnd2  15482  o1lo1  15536  rlimclim1  15544  rlimclim  15545  rlimcn1  15587  rlimcn3  15589  o1of2  15612  o1rlimmul  15618  lo1add  15626  lo1mul  15627  isercolllem1  15664  climcau  15670  caucvgrlem  15672  caucvgb  15679  summolem2  15715  summo  15716  modfsummod  15794  o1fsum  15813  prodmolem2  15937  addmodlteqALT  16331  rpdvds  16666  isprm5  16714  isprm6  16721  pclem  16846  pcqmul  16861  pcexp  16867  pcneg  16882  pcprmpw2  16890  pcadd  16897  pcmpt  16900  4sqlem13  16965  vdwlem2  16990  vdwlem7  16995  vdwlem12  17000  ramval  17016  ramub2  17022  ramz2  17032  ramcl  17037  cshwshashlem2  17104  imasval  17513  imasdsval  17517  mreexexd  17652  acsfn  17663  issubc3  17854  idfucl  17886  funcres2c  17908  isnat  17955  fucpropd  17985  xpcval  18181  xpcco  18187  prfval  18203  evlf2  18222  evlfcl  18226  curf12  18231  curf1cl  18232  curf2  18233  curfcl  18236  curf2ndf  18251  hof2val  18260  hofcl  18263  hofpropd  18271  yonedalem4a  18279  yonedainv  18285  drsdirfi  18309  pospo  18347  poslubmo  18413  posglbmo  18414  isipodrs  18541  acsinfd  18560  chnccat  18630  chnpof1  18634  gsumvalx  18682  gsumpropd2lem  18685  mgmhmeql  18722  sgrppropd  18737  ismndd  18762  mndpropd  18765  mndpsuppss  18771  mhmeql  18832  mndind  18834  frmdup3lem  18872  mhmmnd  19078  issubg4  19159  ssnmz  19179  conjnmzb  19265  f1otrspeq  19459  psgneu  19518  pgpfi  19617  sylow2blem3  19634  slwhash  19636  fislw  19637  sylow3lem2  19640  lsmdisj2  19694  pj1eu  19708  efgredlem  19759  frgpuplem  19784  gexex  19865  frgpnabl  19887  dprdfadd  20034  dpjidcl  20072  pgpfac1lem3  20091  pgpfaclem3  20097  ablfac2  20103  ablsimpgcygd  20120  ablsimpgfind  20124  ablsimpgprmd  20129  rngpropd  20192  ringpropd  20306  imadrhmcl  20815  islmhm2  21074  lmhmpropd  21109  lbsextlem4  21200  prmirredlem  21493  psgndiflemA  21622  lsmcss  21713  uvcf1  21813  frlmsslsp  21817  frlmup1  21819  assapropd  21892  psrval  21936  evlslem1  22104  mamucl  22430  mamuass  22431  mamudi  22432  mamudir  22433  mamuvs1  22434  mamuvs2  22435  mamulid  22470  mamurid  22471  dmatsubcl  22527  dmatmulcl  22529  scmatscm  22542  marrepval  22591  marepveval  22597  mdetunilem7  22647  gsummatr01lem4  22687  cpmatmcllem  22747  mat2pmatf1  22758  mat2pmatlin  22764  decpmatmul  22801  pm2mpmhmlem2  22848  chpidmat  22876  pptbas  23037  toponmre  23122  restbas  23187  iscncl  23298  cnrest2  23315  cnpdis  23322  lmcnp  23333  dishaus  23411  cmpcovf  23420  tgcmp  23430  dfconn2  23448  clsconn  23459  2ndcctbss  23484  dis2ndc  23489  1stccnp  23491  islly2  23513  cldllycmp  23524  locfincmp  23555  comppfsc  23561  kgentopon  23567  txcls  23633  ptpjopn  23641  dfac14  23647  xkoccn  23648  txcnp  23649  txcmpb  23673  txlm  23677  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  qtopcn  23743  qtoprest  23746  regr1lem2  23769  xkocnv  23843  qtophmeo  23846  fmfnfmlem4  23986  hausflim  24010  hauspwpwf1  24016  fclscmp  24059  alexsublem  24073  alexsubALTlem2  24077  alexsubALTlem3  24078  ptcmplem3  24083  ptcmplem4  24084  ptcmplem5  24085  cnextfun  24093  tmdgsum2  24125  symgtgp  24135  tsmsval2  24159  tsmsgsum  24168  utoptop  24263  ismet2  24362  blin  24450  metss2lem  24540  methaus  24549  met1stc  24550  met2ndci  24551  prdsxmslem2  24558  metcnp3  24569  metcnpi3  24575  metustto  24582  metustfbas  24586  nlmvscn  24716  nrginvrcn  24721  xrsxmet  24839  reconnlem1  24856  reconn  24858  xrge0tsms  24864  xmetdcn2  24867  metdscn  24886  addcnlem  24894  fsumcn  24901  cnheiborlem  24985  cnheibor  24986  bndth  24989  lebnum  24995  nmoleub2lem2  25147  ipcn  25277  iscmet3  25324  caubl  25339  rrxdstprj1  25440  minveclem3b  25459  minveclem7  25466  pjthlem2  25469  pmltpc  25481  volfiniun  25578  ioombl1  25593  dyadss  25625  dyaddisjlem  25626  dyadmax  25629  dyadmbllem  25630  opnmbllem  25632  itg1addlem2  25728  itg10a  25741  mbfi1fseqlem6  25751  itg2seq  25773  itg2monolem1  25781  itg2gt0  25791  itgfsum  25858  limcfval  25903  ellimc2  25908  ellimc3  25910  limcres  25917  limciun  25925  dvres  25942  dveflem  26010  rolle  26021  dvlip2  26026  c1liplem1  26027  dvgt0lem1  26033  dvgt0  26035  dvlt0  26036  dvne0  26042  dvfsumrlimge0  26061  ftc1lem6  26072  itgsubst  26080  mdegmullem  26107  ply1domn  26153  ply1divex  26166  fta1g  26199  fta1b  26201  plyf  26227  dgrlem  26258  coeid  26267  plydivalg  26329  aannenlem1  26358  aalioulem3  26364  aalioulem6  26367  abelthlem8  26468  efif1olem4  26576  chordthm  26868  xrlimcnp  26999  jensen  27019  lgamcvglem  27070  lgamcvg2  27085  sqf11  27169  fsumvma2  27244  perfectlem2  27260  lgsdilem  27354  lgsquad2lem2  27415  lgsquad3  27417  2sqlem5  27452  2sqlem9  27457  2sqb  27462  rpvmasumlem  27517  dchrisum0flb  27540  dchrisum0  27550  pntpbnd  27618  pntibndlem3  27622  pntleml  27641  nolt02o  27725  nosupbday  27735  nosupbnd2  27746  noinfbday  27750  noinfbnd2  27761  noetasuplem4  27766  noetainflem4  27770  noetalem1  27771  conway  27838  lesrec  27858  ltslpss  27967  addsprop  28035  bdayons  28335  n0fincut  28414  eucliddivs  28435  remulscllem2  28560  tgjustc1  28610  tgjustc2  28611  legov  28720  legtrid  28726  tglinethru  28771  tglnpt2  28776  tglineintmo  28777  mirreu3  28789  perpcom  28848  colperpexlem3  28867  mideu  28873  opphllem1  28882  hlpasch  28891  lnopp2hpgb  28898  trgcopy  28939  brcgr  29036  brbtwn2  29041  colinearalg  29046  axsegcon  29063  axeuclidlem  29098  axcontlem9  29108  ecgrtg  29119  elntg  29120  eengtrkg  29122  upgr1eopALT  29253  usgredg4  29353  subuhgr  29422  subumgr  29424  usgr2wspthon  30103  clwlkclwwlkf1  30147  eupth2lems  30375  n4cyclfrgr  30428  vacn  30832  blocni  30943  ubthlem3  31010  minvecolem7  31021  chocunii  31439  pjhthmo  31440  pjhthlem2  31530  kbass5  32258  mdsymlem5  32545  foresf1o  32641  fcobij  32861  xrofsup  32908  mgcoval  33114  mgcf1o  33131  xrge0tsmsd  33203  symgcntz  33215  archirngz  33319  archiabllem2a  33324  isarchiofld  33329  prmidl2  33573  mplvrpmmhm  33787  constrelextdg2  33988  smatrcl  34037  reff  34080  ordtconnlem1  34165  qqhval2  34223  volmeas  34472  fiunelcarsg  34557  ballotlemfc0  34734  ballotlemfcc  34735  signstfvneq0  34813  derangenlem  35459  erdsze2lem1  35491  pconnconn  35519  connpconn  35523  cvxsconn  35531  cvmliftmolem2  35570  cvmliftmo  35572  cvmlift2lem10  35600  cvmlift2lem12  35602  cvmlift3lem7  35613  mrsubff1  35802  msubff1  35844  r1peuqusdeg1  35931  ifscgr  36332  cgrxfr  36343  btwnconn1lem13  36387  btwnconn1lem14  36388  outsideofeq  36418  ellines  36440  finminlem  36616  fnejoin2  36667  weiunso  36764  unbdqndv2  36887  irrdiff  37756  qdiff  37757  poimirlem13  38070  poimirlem14  38071  poimirlem32  38089  opnmbllem0  38093  mblfinlem3  38096  itg2addnclem  38108  itg2addnc  38111  ftc1cnnc  38129  upixp  38166  filbcmb  38177  sstotbnd2  38211  isbnd3  38221  prdsbnd2  38232  cntotbnd  38233  ismtyima  38240  bfp  38261  rrncmslem  38269  unichnidl  38468  lshpcmp  39550  islshpat  39579  lfl0f  39631  ishlat3N  39916  3dim1  40029  islvol5  40141  lvoli2  40143  lncvrelatN  40343  pclfinclN  40512  pexmidlem8N  40539  idltrn  40712  cdleme42keg  41048  cdleme42mgN  41050  cdlemf2  41124  cdlemg2cex  41153  trlcoat  41285  dihopelvalcpre  41810  dih1dimatlem  41891  dihjatcclem4  41983  lcfl7N  42063  lcfrlem9  42112  mapdh9a  42351  hdmapglem7  42491  aks4d1p8  42642  isprimroot  42648  evl1gprodd  42672  sticksstones11  42711  grpods  42749  aks5lem8  42756  renegeulemv  42915  sn-subeu  42974  remulinvcom  42980  imacrhmcl  43074  fidomncyc  43091  fsuppind  43110  fsuppssind  43113  mhpind  43114  prjspertr  43125  prjspreln0  43129  flt4lem7  43179  nna4b4nsq  43180  nacsfix  43231  mzpsubst  43267  mzpcompact2lem  43270  eldioph2lem2  43280  eldioph2  43281  eldioph2b  43282  diophin  43291  diophun  43292  irrapxlem3  43339  irrapxlem5  43341  pell1234qrreccl  43369  pell1234qrmulcl  43370  pell14qrdich  43384  pell1qrge1  43385  pell1qrgaplem  43388  monotuz  43456  acongtr  43493  acongrep  43495  jm2.23  43511  jm2.26a  43515  jm2.26lem3  43516  jm2.26  43517  jm2.27  43523  wepwsolem  43557  fnwe2lem2  43566  kelac1  43578  kercvrlsm  43598  hbtlem5  43643  hbt  43645  mpaaeu  43665  cantnfresb  43839  onmcl  43846  tfsconcatun  43852  tfsconcatfn  43853  tfsconcatfv1  43854  tfsconcatfv2  43855  naddcnff  43877  rfovcnvf1od  44518  mnurndlem1  44795  cncmpmax  45550  rfcnnnub  45554  disjxp1  45587  iccintsng  46037  fprodcn  46114  lptioo2  46145  lptioo1  46146  limclner  46163  stoweidlem31  46543  stoweidlem34  46546  stoweidlem35  46547  stoweidlem49  46561  stoweidlem59  46571  stoweidlem62  46574  fourierdlem60  46678  fourierdlem61  46679  fourierdlem87  46705  iundjiun  46972  ismeannd  46979  hoidmvle  47112  smfsuplem2  47324  2reu8i  47645  prproropf1olem2  48048  paireqne  48055  nprmmul2  48072  perfectALTVlem2  48282  mogoldbb  48345  bgoldbtbndlem2  48366  bgoldbtbndlem3  48367  grimedg  48495  grlimprclnbgrvtx  48559  scmsuppss  48931  lindslinindsimp2lem5  49022  elfzolborelfzop1  49079  elbigolo1  49117  itschlc0xyqsol1  49326  itschlc0xyqsol  49327  iccdisj  49457  toslat  49541  iinfssclem3  49615  iinfssc  49616  iinfsubc  49617  imasubc3  49715  upciclem4  49728  uppropd  49740  natoppf  49788  tposcurf1  49858  fuco22  49898  fuco22natlem  49904  functhinclem4  50006  arweuthinc  50088