Theorem simplrr 778

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 728	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  5083  frpomin  6296  fsnex  7229  f1prex  7230  isotr  7282  weniso  7300  riota5f  7343  frxp2  8085  frxp3  8092  xpord3pred  8093  poseq  8099  fprlem2  8242  tfrlem9a  8316  oaass  8487  oeeui  8529  oaabs2  8576  coflton  8598  cofon1  8599  naddssim  8612  resixpfo  8875  omxpenlem  9007  pw2f1olem  9010  fopwdom  9014  fofinf1o  9233  marypha1lem  9337  ordiso2  9421  oismo  9446  ixpiunwdom  9496  cantnf  9603  ttrclss  9630  fseqenlem1  9935  iunfictbso  10025  dfac12lem2  10056  dfac12lem3  10057  infunsdom1  10123  infpssrlem5  10218  fin23lem24  10233  isf32lem2  10265  isf32lem4  10267  isf34lem4  10288  fin1a2lem12  10322  fin1a2lem13  10323  ttukeylem6  10425  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  winalim2  10608  wunex2  10650  tskord  10692  prlem934  10945  mulcmpblnr  10983  dedekind  11297  addrid  11314  cnegex  11315  negeu  11371  add20  11650  divdivdiv  11843  ltmul12a  11998  lemul12a  12000  lediv12a  12036  supaddc  12110  supmul1  12112  cru  12138  uzwo3  12857  xleadd1a  13169  xmullem  13180  xmulgt0  13199  xlemul1a  13204  ixxun  13278  ixxss12  13282  ioodisj  13399  fz0fzelfz0  13551  mulexpz  14026  rpexpmord  14092  leexp1a  14099  expmulnbnd  14159  hashf1  14381  fi1uzind  14431  brfi1indALT  14434  swrdccat  14659  reuccatpfxs1  14671  abs3lem  15263  rexanre  15271  cau3lem  15279  limsupgre  15405  limsupbnd2  15407  o1lo1  15461  rlimclim1  15469  rlimclim  15470  rlimcn1  15512  rlimcn3  15514  o1of2  15537  o1rlimmul  15543  lo1add  15551  lo1mul  15552  isercolllem1  15589  climcau  15595  caucvgrlem  15597  caucvgb  15604  summolem2  15640  summo  15641  modfsummod  15718  o1fsum  15737  prodmolem2  15859  addmodlteqALT  16253  rpdvds  16588  isprm5  16635  isprm6  16642  pclem  16767  pcqmul  16782  pcexp  16788  pcneg  16803  pcprmpw2  16811  pcadd  16818  pcmpt  16821  4sqlem13  16886  vdwlem2  16911  vdwlem7  16916  vdwlem12  16921  ramval  16937  ramub2  16943  ramz2  16953  ramcl  16958  cshwshashlem2  17025  imasval  17433  imasdsval  17437  mreexexd  17572  acsfn  17583  issubc3  17774  idfucl  17806  funcres2c  17828  isnat  17875  fucpropd  17905  xpcval  18101  xpcco  18107  prfval  18123  evlf2  18142  evlfcl  18146  curf12  18151  curf1cl  18152  curf2  18153  curfcl  18156  curf2ndf  18171  hof2val  18180  hofcl  18183  hofpropd  18191  yonedalem4a  18199  yonedainv  18205  drsdirfi  18229  pospo  18267  poslubmo  18333  posglbmo  18334  isipodrs  18461  acsinfd  18480  chnccat  18550  chnpof1  18554  gsumvalx  18602  gsumpropd2lem  18605  mgmhmeql  18642  sgrppropd  18657  ismndd  18682  mndpropd  18685  mndpsuppss  18691  mhmeql  18752  mndind  18754  frmdup3lem  18792  mhmmnd  18998  issubg4  19079  ssnmz  19099  conjnmzb  19186  f1otrspeq  19380  psgneu  19439  pgpfi  19538  sylow2blem3  19555  slwhash  19557  fislw  19558  sylow3lem2  19561  lsmdisj2  19615  pj1eu  19629  efgredlem  19680  frgpuplem  19705  gexex  19786  frgpnabl  19808  dprdfadd  19955  dpjidcl  19993  pgpfac1lem3  20012  pgpfaclem3  20018  ablfac2  20024  ablsimpgcygd  20041  ablsimpgfind  20045  ablsimpgprmd  20050  rngpropd  20113  ringpropd  20227  imadrhmcl  20732  islmhm2  20992  lmhmpropd  21027  lbsextlem4  21118  prmirredlem  21429  psgndiflemA  21558  lsmcss  21649  uvcf1  21749  frlmsslsp  21753  frlmup1  21755  assapropd  21828  psrval  21872  evlslem1  22038  mamucl  22344  mamuass  22345  mamudi  22346  mamudir  22347  mamuvs1  22348  mamuvs2  22349  mamulid  22384  mamurid  22385  dmatsubcl  22441  dmatmulcl  22443  scmatscm  22456  marrepval  22505  marepveval  22511  mdetunilem7  22561  gsummatr01lem4  22601  cpmatmcllem  22661  mat2pmatf1  22672  mat2pmatlin  22678  decpmatmul  22715  pm2mpmhmlem2  22762  chpidmat  22790  pptbas  22951  toponmre  23036  restbas  23101  iscncl  23212  cnrest2  23229  cnpdis  23236  lmcnp  23247  dishaus  23325  cmpcovf  23334  tgcmp  23344  dfconn2  23362  clsconn  23373  2ndcctbss  23398  dis2ndc  23403  1stccnp  23405  islly2  23427  cldllycmp  23438  locfincmp  23469  comppfsc  23475  kgentopon  23481  txcls  23547  ptpjopn  23555  dfac14  23561  xkoccn  23562  txcnp  23563  txcmpb  23587  txlm  23591  xkopt  23598  xkoco1cn  23600  xkoco2cn  23601  qtopcn  23657  qtoprest  23660  regr1lem2  23683  xkocnv  23757  qtophmeo  23760  fmfnfmlem4  23900  hausflim  23924  hauspwpwf1  23930  fclscmp  23973  alexsublem  23987  alexsubALTlem2  23991  alexsubALTlem3  23992  ptcmplem3  23997  ptcmplem4  23998  ptcmplem5  23999  cnextfun  24007  tmdgsum2  24039  symgtgp  24049  tsmsval2  24073  tsmsgsum  24082  utoptop  24177  ismet2  24276  blin  24364  metss2lem  24454  methaus  24463  met1stc  24464  met2ndci  24465  prdsxmslem2  24472  metcnp3  24483  metcnpi3  24489  metustto  24496  metustfbas  24500  nlmvscn  24630  nrginvrcn  24635  xrsxmet  24753  reconnlem1  24770  reconn  24772  xrge0tsms  24778  xmetdcn2  24781  metdscn  24800  addcnlem  24808  fsumcn  24815  cnheiborlem  24899  cnheibor  24900  bndth  24903  lebnum  24909  nmoleub2lem2  25061  ipcn  25191  iscmet3  25238  caubl  25253  rrxdstprj1  25354  minveclem3b  25373  minveclem7  25380  pjthlem2  25383  pmltpc  25395  volfiniun  25492  ioombl1  25507  dyadss  25539  dyaddisjlem  25540  dyadmax  25543  dyadmbllem  25544  opnmbllem  25546  itg1addlem2  25642  itg10a  25655  mbfi1fseqlem6  25665  itg2seq  25687  itg2monolem1  25695  itg2gt0  25705  itgfsum  25772  limcfval  25817  ellimc2  25822  ellimc3  25824  limcres  25831  limciun  25839  dvres  25856  dveflem  25924  rolle  25935  dvlip2  25941  c1liplem1  25942  dvgt0lem1  25948  dvgt0  25950  dvlt0  25951  dvne0  25957  dvfsumrlimge0  25978  ftc1lem6  25989  itgsubst  25997  mdegmullem  26024  ply1domn  26070  ply1divex  26083  fta1g  26116  fta1b  26118  plyf  26144  dgrlem  26175  coeid  26184  plydivalg  26247  aannenlem1  26276  aalioulem3  26282  aalioulem6  26285  abelthlem8  26389  efif1olem4  26494  chordthm  26787  xrlimcnp  26918  jensen  26939  lgamcvglem  26990  lgamcvg2  27005  sqf11  27089  fsumvma2  27165  perfectlem2  27181  lgsdilem  27275  lgsquad2lem2  27336  lgsquad3  27338  2sqlem5  27373  2sqlem9  27378  2sqb  27383  rpvmasumlem  27438  dchrisum0flb  27461  dchrisum0  27471  pntpbnd  27539  pntibndlem3  27543  pntleml  27562  nolt02o  27647  nosupbday  27657  nosupbnd2  27668  noinfbday  27672  noinfbnd2  27683  noetasuplem4  27688  noetainflem4  27692  noetalem1  27693  conway  27759  lesrec  27779  ltslpss  27888  addsprop  27956  bdayons  28256  n0fincut  28335  eucliddivs  28356  remulscllem2  28481  tgjustc1  28531  tgjustc2  28532  legov  28641  legtrid  28647  tglinethru  28692  tglnpt2  28697  tglineintmo  28698  mirreu3  28710  perpcom  28769  colperpexlem3  28788  mideu  28794  opphllem1  28803  hlpasch  28812  lnopp2hpgb  28819  trgcopy  28860  brcgr  28957  brbtwn2  28962  colinearalg  28967  axsegcon  28984  axeuclidlem  29019  axcontlem9  29029  ecgrtg  29040  elntg  29041  eengtrkg  29043  upgr1eopALT  29174  usgredg4  29274  subuhgr  29343  subumgr  29345  usgr2wspthon  30025  clwlkclwwlkf1  30069  eupth2lems  30297  n4cyclfrgr  30350  vacn  30754  blocni  30865  ubthlem3  30932  minvecolem7  30943  chocunii  31361  pjhthmo  31362  pjhthlem2  31452  kbass5  32180  mdsymlem5  32467  foresf1o  32563  fcobij  32782  xrofsup  32830  mgcoval  33051  mgcf1o  33068  xrge0tsmsd  33139  symgcntz  33151  archirngz  33255  archiabllem2a  33260  isarchiofld  33265  prmidl2  33506  mplvrpmmhm  33695  constrelextdg2  33897  smatrcl  33946  reff  33989  ordtconnlem1  34074  qqhval2  34132  volmeas  34381  fiunelcarsg  34466  ballotlemfc0  34643  ballotlemfcc  34644  signstfvneq0  34722  derangenlem  35359  erdsze2lem1  35391  pconnconn  35419  connpconn  35423  cvxsconn  35431  cvmliftmolem2  35470  cvmliftmo  35472  cvmlift2lem10  35500  cvmlift2lem12  35502  cvmlift3lem7  35513  mrsubff1  35702  msubff1  35744  r1peuqusdeg1  35831  ifscgr  36232  cgrxfr  36243  btwnconn1lem13  36287  btwnconn1lem14  36288  outsideofeq  36318  ellines  36340  finminlem  36506  fnejoin2  36557  weiunso  36654  unbdqndv2  36769  irrdiff  37638  poimirlem13  37945  poimirlem14  37946  poimirlem32  37964  opnmbllem0  37968  mblfinlem3  37971  itg2addnclem  37983  itg2addnc  37986  ftc1cnnc  38004  upixp  38041  filbcmb  38052  sstotbnd2  38086  isbnd3  38096  prdsbnd2  38107  cntotbnd  38108  ismtyima  38115  bfp  38136  rrncmslem  38144  unichnidl  38343  lshpcmp  39425  islshpat  39454  lfl0f  39506  ishlat3N  39791  3dim1  39904  islvol5  40016  lvoli2  40018  lncvrelatN  40218  pclfinclN  40387  pexmidlem8N  40414  idltrn  40587  cdleme42keg  40923  cdleme42mgN  40925  cdlemf2  40999  cdlemg2cex  41028  trlcoat  41160  dihopelvalcpre  41685  dih1dimatlem  41766  dihjatcclem4  41858  lcfl7N  41938  lcfrlem9  41987  mapdh9a  42226  hdmapglem7  42366  aks4d1p8  42518  isprimroot  42524  evl1gprodd  42548  sticksstones11  42587  grpods  42625  aks5lem8  42632  renegeulemv  42799  sn-subeu  42858  remulinvcom  42864  imacrhmcl  42958  fidomncyc  42979  fsuppind  43022  fsuppssind  43025  mhpind  43026  prjspertr  43037  prjspreln0  43041  flt4lem7  43091  nna4b4nsq  43092  nacsfix  43143  mzpsubst  43179  mzpcompact2lem  43182  eldioph2lem2  43192  eldioph2  43193  eldioph2b  43194  diophin  43203  diophun  43204  irrapxlem3  43255  irrapxlem5  43257  pell1234qrreccl  43285  pell1234qrmulcl  43286  pell14qrdich  43300  pell1qrge1  43301  pell1qrgaplem  43304  monotuz  43372  acongtr  43409  acongrep  43411  jm2.23  43427  jm2.26a  43431  jm2.26lem3  43432  jm2.26  43433  jm2.27  43439  wepwsolem  43473  fnwe2lem2  43482  kelac1  43494  kercvrlsm  43514  hbtlem5  43559  hbt  43561  mpaaeu  43581  cantnfresb  43755  onmcl  43762  tfsconcatun  43768  tfsconcatfn  43769  tfsconcatfv1  43770  tfsconcatfv2  43771  naddcnff  43793  rfovcnvf1od  44434  mnurndlem1  44711  cncmpmax  45466  rfcnnnub  45470  disjxp1  45503  iccintsng  45957  fprodcn  46034  lptioo2  46065  lptioo1  46066  limclner  46083  stoweidlem31  46463  stoweidlem34  46466  stoweidlem35  46467  stoweidlem49  46481  stoweidlem59  46491  stoweidlem62  46494  fourierdlem60  46598  fourierdlem61  46599  fourierdlem87  46625  iundjiun  46892  ismeannd  46899  hoidmvle  47032  smfsuplem2  47244  2reu8i  47547  prproropf1olem2  47938  paireqne  47945  perfectALTVlem2  48156  mogoldbb  48219  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  grimedg  48369  grlimprclnbgrvtx  48433  scmsuppss  48805  lindslinindsimp2lem5  48896  elfzolborelfzop1  48953  elbigolo1  48991  itschlc0xyqsol1  49200  itschlc0xyqsol  49201  iccdisj  49331  toslat  49415  iinfssclem3  49489  iinfssc  49490  iinfsubc  49491  imasubc3  49589  upciclem4  49602  uppropd  49614  natoppf  49662  tposcurf1  49732  fuco22  49772  fuco22natlem  49778  functhinclem4  49880  arweuthinc  49962