Theorem simplrr 775

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  disjxiun  5089  frpomin  6279  fsnex  7211  f1prex  7212  isotr  7263  weniso  7281  riota5f  7322  poseq  8045  fprlem2  8187  tfrlem9a  8287  oaass  8463  oeeui  8504  oaabs2  8550  resixpfo  8795  omxpenlem  8938  pw2f1olem  8941  fopwdom  8945  fofinf1o  9192  marypha1lem  9290  ordiso2  9372  oismo  9397  ixpiunwdom  9447  cantnf  9550  ttrclss  9577  fseqenlem1  9881  iunfictbso  9971  dfac12lem2  10001  dfac12lem3  10002  infunsdom1  10070  infpssrlem5  10164  fin23lem24  10179  isf32lem2  10211  isf32lem4  10213  isf34lem4  10234  fin1a2lem12  10268  fin1a2lem13  10269  ttukeylem6  10371  fpwwe2lem11  10498  fpwwe2lem12  10499  fpwwe2  10500  winalim2  10553  wunex2  10595  tskord  10637  prlem934  10890  mulcmpblnr  10928  dedekind  11239  addid1  11256  cnegex  11257  negeu  11312  add20  11588  divdivdiv  11777  ltmul12a  11932  lemul12a  11934  lediv12a  11969  supaddc  12043  supmul1  12045  cru  12066  uzwo3  12784  xleadd1a  13088  xmullem  13099  xmulgt0  13118  xlemul1a  13123  ixxun  13196  ixxss12  13200  ioodisj  13315  fz0fzelfz0  13463  mulexpz  13924  rpexpmord  13987  leexp1a  13994  expmulnbnd  14051  hashf1  14271  fi1uzind  14311  brfi1indALT  14314  swrdccat  14546  reuccatpfxs1  14558  abs3lem  15149  rexanre  15157  cau3lem  15165  limsupgre  15289  limsupbnd2  15291  o1lo1  15345  rlimclim1  15353  rlimclim  15354  rlimcn1  15396  rlimcn3  15398  o1of2  15421  o1rlimmul  15427  lo1add  15435  lo1mul  15436  isercolllem1  15475  climcau  15481  caucvgrlem  15483  caucvgb  15490  summolem2  15527  summo  15528  modfsummod  15605  o1fsum  15624  prodmolem2  15744  addmodlteqALT  16133  rpdvds  16462  isprm5  16509  isprm6  16516  pclem  16636  pcqmul  16651  pcexp  16657  pcneg  16672  pcprmpw2  16680  pcadd  16687  pcmpt  16690  4sqlem13  16755  vdwlem2  16780  vdwlem7  16785  vdwlem12  16790  ramval  16806  ramub2  16812  ramz2  16822  ramcl  16827  cshwshashlem2  16895  imasval  17319  imasdsval  17323  mreexexd  17454  acsfn  17465  issubc3  17661  idfucl  17693  funcres2c  17714  isnat  17760  fucpropd  17792  xpcval  17991  xpcco  17997  prfval  18013  evlf2  18033  evlfcl  18037  curf12  18042  curf1cl  18043  curf2  18044  curfcl  18047  curf2ndf  18062  hof2val  18071  hofcl  18074  hofpropd  18082  yonedalem4a  18090  yonedainv  18096  drsdirfi  18120  pospo  18160  poslubmo  18226  posglbmo  18227  isipodrs  18352  acsinfd  18371  gsumvalx  18457  gsumpropd2lem  18460  ismndd  18504  mndpropd  18507  mhmeql  18561  mndind  18563  frmdup3lem  18601  mhmmnd  18793  issubg4  18870  ssnmz  18890  conjnmzb  18965  f1otrspeq  19151  psgneu  19210  pgpfi  19306  sylow2blem3  19323  slwhash  19325  fislw  19326  sylow3lem2  19329  lsmdisj2  19383  pj1eu  19397  efgredlem  19448  frgpuplem  19473  gexex  19549  frgpnabl  19571  dprdfadd  19718  dpjidcl  19756  pgpfac1lem3  19775  pgpfaclem3  19781  ablfac2  19787  ablsimpgcygd  19804  ablsimpgfind  19808  ablsimpgprmd  19813  ringpropd  19916  islmhm2  20406  lmhmpropd  20441  lbsextlem4  20529  prmirredlem  20800  psgndiflemA  20912  lsmcss  21003  uvcf1  21105  frlmsslsp  21109  frlmup1  21111  assapropd  21182  psrval  21224  evlslem1  21398  mamucl  21654  mamuass  21655  mamudi  21656  mamudir  21657  mamuvs1  21658  mamuvs2  21659  mamulid  21696  mamurid  21697  dmatsubcl  21753  dmatmulcl  21755  scmatscm  21768  marrepval  21817  marepveval  21823  mdetunilem7  21873  gsummatr01lem4  21913  cpmatmcllem  21973  mat2pmatf1  21984  mat2pmatlin  21990  decpmatmul  22027  pm2mpmhmlem2  22074  chpidmat  22102  pptbas  22264  toponmre  22350  restbas  22415  iscncl  22526  cnrest2  22543  cnpdis  22550  lmcnp  22561  dishaus  22639  cmpcovf  22648  tgcmp  22658  dfconn2  22676  clsconn  22687  2ndcctbss  22712  dis2ndc  22717  1stccnp  22719  islly2  22741  cldllycmp  22752  locfincmp  22783  comppfsc  22789  kgentopon  22795  txcls  22861  ptpjopn  22869  dfac14  22875  xkoccn  22876  txcnp  22877  txcmpb  22901  txlm  22905  xkopt  22912  xkoco1cn  22914  xkoco2cn  22915  qtopcn  22971  qtoprest  22974  regr1lem2  22997  xkocnv  23071  qtophmeo  23074  fmfnfmlem4  23214  hausflim  23238  hauspwpwf1  23244  fclscmp  23287  alexsublem  23301  alexsubALTlem2  23305  alexsubALTlem3  23306  ptcmplem3  23311  ptcmplem4  23312  ptcmplem5  23313  cnextfun  23321  tmdgsum2  23353  symgtgp  23363  tsmsval2  23387  tsmsgsum  23396  utoptop  23492  ismet2  23592  blin  23680  metss2lem  23773  methaus  23782  met1stc  23783  met2ndci  23784  prdsxmslem2  23791  metcnp3  23802  metcnpi3  23808  metustto  23815  metustfbas  23819  nlmvscn  23957  nrginvrcn  23962  xrsxmet  24078  reconnlem1  24095  reconn  24097  xrge0tsms  24103  xmetdcn2  24106  metdscn  24125  addcnlem  24133  fsumcn  24139  cnheiborlem  24223  cnheibor  24224  bndth  24227  lebnum  24233  nmoleub2lem2  24385  ipcn  24516  iscmet3  24563  caubl  24578  rrxdstprj1  24679  minveclem3b  24698  minveclem7  24705  pjthlem2  24708  pmltpc  24720  volfiniun  24817  ioombl1  24832  dyadss  24864  dyaddisjlem  24865  dyadmax  24868  dyadmbllem  24869  opnmbllem  24871  itg1addlem2  24967  itg10a  24981  mbfi1fseqlem6  24991  itg2seq  25013  itg2monolem1  25021  itg2gt0  25031  itgfsum  25097  limcfval  25142  ellimc2  25147  ellimc3  25149  limcres  25156  limciun  25164  dvres  25181  dveflem  25249  rolle  25260  dvlip2  25265  c1liplem1  25266  dvgt0lem1  25272  dvgt0  25274  dvlt0  25275  dvne0  25281  dvfsumrlimge0  25300  ftc1lem6  25311  itgsubst  25319  mdegmullem  25349  ply1domn  25394  ply1divex  25407  fta1g  25438  fta1b  25440  plyf  25465  dgrlem  25496  coeid  25505  plydivalg  25565  aannenlem1  25594  aalioulem3  25600  aalioulem6  25603  abelthlem8  25704  efif1olem4  25807  chordthm  26093  xrlimcnp  26224  jensen  26244  lgamcvglem  26295  lgamcvg2  26310  sqf11  26394  fsumvma2  26468  perfectlem2  26484  lgsdilem  26578  lgsquad2lem2  26639  lgsquad3  26641  2sqlem5  26676  2sqlem9  26681  2sqb  26686  rpvmasumlem  26741  dchrisum0flb  26764  dchrisum0  26774  pntpbnd  26842  pntibndlem3  26846  pntleml  26865  nolt02o  26949  nosupbday  26959  nosupbnd2  26970  noinfbday  26974  noinfbnd2  26985  noetasuplem4  26990  noetainflem4  26994  noetalem1  26995  conway  27044  slerec  27064  tgjustc1  27125  tgjustc2  27126  legov  27235  legtrid  27241  tglinethru  27286  tglnpt2  27291  tglineintmo  27292  mirreu3  27304  perpcom  27363  colperpexlem3  27382  mideu  27388  opphllem1  27397  hlpasch  27406  lnopp2hpgb  27413  trgcopy  27454  brcgr  27557  brbtwn2  27562  colinearalg  27567  axsegcon  27584  axeuclidlem  27619  axcontlem9  27629  ecgrtg  27640  elntg  27641  eengtrkg  27643  upgr1eopALT  27776  usgredg4  27873  subuhgr  27942  subumgr  27944  usgr2wspthon  28618  clwlkclwwlkf1  28662  eupth2lems  28890  n4cyclfrgr  28943  vacn  29344  blocni  29455  ubthlem3  29522  minvecolem7  29533  chocunii  29951  pjhthmo  29952  pjhthlem2  30042  kbass5  30770  mdsymlem5  31057  foresf1o  31138  fcobij  31344  xrofsup  31377  mgcoval  31551  mgcf1o  31568  xrge0tsmsd  31604  symgcntz  31641  archirngz  31730  archiabllem2a  31735  isarchiofld  31816  prmidl2  31913  smatrcl  32044  reff  32087  ordtconnlem1  32172  qqhval2  32230  volmeas  32497  fiunelcarsg  32583  ballotlemfc0  32759  ballotlemfcc  32760  signstfvneq0  32851  derangenlem  33432  erdsze2lem1  33464  pconnconn  33492  connpconn  33496  cvxsconn  33504  cvmliftmolem2  33543  cvmliftmo  33545  cvmlift2lem10  33573  cvmlift2lem12  33575  cvmlift3lem7  33586  mrsubff1  33775  msubff1  33817  frxp2  34073  frxp3  34079  naddssim  34116  sltlpss  34183  ifscgr  34442  cgrxfr  34453  btwnconn1lem13  34497  btwnconn1lem14  34498  outsideofeq  34528  ellines  34550  finminlem  34603  fnejoin2  34654  unbdqndv2  34787  irrdiff  35602  poimirlem13  35895  poimirlem14  35896  poimirlem32  35914  opnmbllem0  35918  mblfinlem3  35921  itg2addnclem  35933  itg2addnc  35936  ftc1cnnc  35954  upixp  35992  filbcmb  36003  sstotbnd2  36037  isbnd3  36047  prdsbnd2  36058  cntotbnd  36059  ismtyima  36066  bfp  36087  rrncmslem  36095  unichnidl  36294  lshpcmp  37255  islshpat  37284  lfl0f  37336  ishlat3N  37621  3dim1  37735  islvol5  37847  lvoli2  37849  lncvrelatN  38049  pclfinclN  38218  pexmidlem8N  38245  idltrn  38418  cdleme42keg  38754  cdleme42mgN  38756  cdlemf2  38830  cdlemg2cex  38859  trlcoat  38991  dihopelvalcpre  39516  dih1dimatlem  39597  dihjatcclem4  39689  lcfl7N  39769  lcfrlem9  39818  mapdh9a  40057  hdmapglem7  40197  aks4d1p8  40349  sticksstones11  40369  rncrhmcl  40500  fsuppind  40539  fsuppssind  40542  mhpind  40543  mhphf  40545  renegeulemv  40611  sn-subeu  40668  remulinvcom  40674  itrere  40696  retire  40697  prjspertr  40704  prjspreln0  40708  flt4lem7  40758  nna4b4nsq  40759  nacsfix  40796  mzpsubst  40832  mzpcompact2lem  40835  eldioph2lem2  40845  eldioph2  40846  eldioph2b  40847  diophin  40856  diophun  40857  irrapxlem3  40908  irrapxlem5  40910  pell1234qrreccl  40938  pell1234qrmulcl  40939  pell14qrdich  40953  pell1qrge1  40954  pell1qrgaplem  40957  monotuz  41026  acongtr  41063  acongrep  41065  jm2.23  41081  jm2.26a  41085  jm2.26lem3  41086  jm2.26  41087  jm2.27  41093  wepwsolem  41130  fnwe2lem2  41139  kelac1  41151  kercvrlsm  41171  hbtlem5  41216  hbt  41218  mpaaeu  41238  naddcnff  41328  rfovcnvf1od  41933  mnurndlem1  42220  cncmpmax  42896  rfcnnnub  42900  disjxp1  42937  iccintsng  43397  fprodcn  43477  lptioo2  43508  lptioo1  43509  limclner  43528  stoweidlem31  43908  stoweidlem34  43911  stoweidlem35  43912  stoweidlem49  43926  stoweidlem59  43936  stoweidlem62  43939  fourierdlem60  44043  fourierdlem61  44044  fourierdlem87  44070  iundjiun  44335  ismeannd  44342  hoidmvle  44475  smfsuplem2  44687  2reu8i  44956  prproropf1olem2  45307  paireqne  45314  perfectALTVlem2  45525  mogoldbb  45588  bgoldbtbndlem2  45609  bgoldbtbndlem3  45610  isomgrtrlem  45641  mgmhmeql  45708  mndpsuppss  46058  scmsuppss  46059  lindslinindsimp2lem5  46154  elfzolborelfzop1  46211  elbigolo1  46254  itschlc0xyqsol1  46463  itschlc0xyqsol  46464  iccdisj  46543  toslat  46619  functhinclem4  46676