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  5096  frpomin  6299  fsnex  7231  f1prex  7232  isotr  7284  weniso  7302  riota5f  7345  frxp2  8088  frxp3  8095  xpord3pred  8096  poseq  8102  fprlem2  8245  tfrlem9a  8319  oaass  8490  oeeui  8532  oaabs2  8579  coflton  8601  cofon1  8602  naddssim  8615  resixpfo  8878  omxpenlem  9010  pw2f1olem  9013  fopwdom  9017  fofinf1o  9236  marypha1lem  9340  ordiso2  9424  oismo  9449  ixpiunwdom  9499  cantnf  9606  ttrclss  9633  fseqenlem1  9938  iunfictbso  10028  dfac12lem2  10059  dfac12lem3  10060  infunsdom1  10126  infpssrlem5  10221  fin23lem24  10236  isf32lem2  10268  isf32lem4  10270  isf34lem4  10291  fin1a2lem12  10325  fin1a2lem13  10326  ttukeylem6  10428  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  winalim2  10611  wunex2  10653  tskord  10695  prlem934  10948  mulcmpblnr  10986  dedekind  11300  addrid  11317  cnegex  11318  negeu  11374  add20  11653  divdivdiv  11846  ltmul12a  12001  lemul12a  12003  lediv12a  12039  supaddc  12113  supmul1  12115  cru  12141  uzwo3  12860  xleadd1a  13172  xmullem  13183  xmulgt0  13202  xlemul1a  13207  ixxun  13281  ixxss12  13285  ioodisj  13402  fz0fzelfz0  13554  mulexpz  14029  rpexpmord  14095  leexp1a  14102  expmulnbnd  14162  hashf1  14384  fi1uzind  14434  brfi1indALT  14437  swrdccat  14662  reuccatpfxs1  14674  abs3lem  15266  rexanre  15274  cau3lem  15282  limsupgre  15408  limsupbnd2  15410  o1lo1  15464  rlimclim1  15472  rlimclim  15473  rlimcn1  15515  rlimcn3  15517  o1of2  15540  o1rlimmul  15546  lo1add  15554  lo1mul  15555  isercolllem1  15592  climcau  15598  caucvgrlem  15600  caucvgb  15607  summolem2  15643  summo  15644  modfsummod  15721  o1fsum  15740  prodmolem2  15862  addmodlteqALT  16256  rpdvds  16591  isprm5  16638  isprm6  16645  pclem  16770  pcqmul  16785  pcexp  16791  pcneg  16806  pcprmpw2  16814  pcadd  16821  pcmpt  16824  4sqlem13  16889  vdwlem2  16914  vdwlem7  16919  vdwlem12  16924  ramval  16940  ramub2  16946  ramz2  16956  ramcl  16961  cshwshashlem2  17028  imasval  17436  imasdsval  17440  mreexexd  17575  acsfn  17586  issubc3  17777  idfucl  17809  funcres2c  17831  isnat  17878  fucpropd  17908  xpcval  18104  xpcco  18110  prfval  18126  evlf2  18145  evlfcl  18149  curf12  18154  curf1cl  18155  curf2  18156  curfcl  18159  curf2ndf  18174  hof2val  18183  hofcl  18186  hofpropd  18194  yonedalem4a  18202  yonedainv  18208  drsdirfi  18232  pospo  18270  poslubmo  18336  posglbmo  18337  isipodrs  18464  acsinfd  18483  chnccat  18553  chnpof1  18557  gsumvalx  18605  gsumpropd2lem  18608  mgmhmeql  18645  sgrppropd  18660  ismndd  18685  mndpropd  18688  mndpsuppss  18694  mhmeql  18755  mndind  18757  frmdup3lem  18795  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  20734  islmhm2  20994  lmhmpropd  21029  lbsextlem4  21120  prmirredlem  21431  psgndiflemA  21560  lsmcss  21651  uvcf1  21751  frlmsslsp  21755  frlmup1  21757  assapropd  21831  psrval  21875  evlslem1  22041  mamucl  22349  mamuass  22350  mamudi  22351  mamudir  22352  mamuvs1  22353  mamuvs2  22354  mamulid  22389  mamurid  22390  dmatsubcl  22446  dmatmulcl  22448  scmatscm  22461  marrepval  22510  marepveval  22516  mdetunilem7  22566  gsummatr01lem4  22606  cpmatmcllem  22666  mat2pmatf1  22677  mat2pmatlin  22683  decpmatmul  22720  pm2mpmhmlem2  22767  chpidmat  22795  pptbas  22956  toponmre  23041  restbas  23106  iscncl  23217  cnrest2  23234  cnpdis  23241  lmcnp  23252  dishaus  23330  cmpcovf  23339  tgcmp  23349  dfconn2  23367  clsconn  23378  2ndcctbss  23403  dis2ndc  23408  1stccnp  23410  islly2  23432  cldllycmp  23443  locfincmp  23474  comppfsc  23480  kgentopon  23486  txcls  23552  ptpjopn  23560  dfac14  23566  xkoccn  23567  txcnp  23568  txcmpb  23592  txlm  23596  xkopt  23603  xkoco1cn  23605  xkoco2cn  23606  qtopcn  23662  qtoprest  23665  regr1lem2  23688  xkocnv  23762  qtophmeo  23765  fmfnfmlem4  23905  hausflim  23929  hauspwpwf1  23935  fclscmp  23978  alexsublem  23992  alexsubALTlem2  23996  alexsubALTlem3  23997  ptcmplem3  24002  ptcmplem4  24003  ptcmplem5  24004  cnextfun  24012  tmdgsum2  24044  symgtgp  24054  tsmsval2  24078  tsmsgsum  24087  utoptop  24182  ismet2  24281  blin  24369  metss2lem  24459  methaus  24468  met1stc  24469  met2ndci  24470  prdsxmslem2  24477  metcnp3  24488  metcnpi3  24494  metustto  24501  metustfbas  24505  nlmvscn  24635  nrginvrcn  24640  xrsxmet  24758  reconnlem1  24775  reconn  24777  xrge0tsms  24783  xmetdcn2  24786  metdscn  24805  addcnlem  24813  fsumcn  24821  cnheiborlem  24913  cnheibor  24914  bndth  24917  lebnum  24923  nmoleub2lem2  25076  ipcn  25206  iscmet3  25253  caubl  25268  rrxdstprj1  25369  minveclem3b  25388  minveclem7  25395  pjthlem2  25398  pmltpc  25411  volfiniun  25508  ioombl1  25523  dyadss  25555  dyaddisjlem  25556  dyadmax  25559  dyadmbllem  25560  opnmbllem  25562  itg1addlem2  25658  itg10a  25671  mbfi1fseqlem6  25681  itg2seq  25703  itg2monolem1  25711  itg2gt0  25721  itgfsum  25788  limcfval  25833  ellimc2  25838  ellimc3  25840  limcres  25847  limciun  25855  dvres  25872  dveflem  25943  rolle  25954  dvlip2  25960  c1liplem1  25961  dvgt0lem1  25967  dvgt0  25969  dvlt0  25970  dvne0  25976  dvfsumrlimge0  25997  ftc1lem6  26008  itgsubst  26016  mdegmullem  26043  ply1domn  26089  ply1divex  26102  fta1g  26135  fta1b  26137  plyf  26163  dgrlem  26194  coeid  26203  plydivalg  26267  aannenlem1  26296  aalioulem3  26302  aalioulem6  26305  abelthlem8  26409  efif1olem4  26514  chordthm  26807  xrlimcnp  26938  jensen  26959  lgamcvglem  27010  lgamcvg2  27025  sqf11  27109  fsumvma2  27185  perfectlem2  27201  lgsdilem  27295  lgsquad2lem2  27356  lgsquad3  27358  2sqlem5  27393  2sqlem9  27398  2sqb  27403  rpvmasumlem  27458  dchrisum0flb  27481  dchrisum0  27491  pntpbnd  27559  pntibndlem3  27563  pntleml  27582  nolt02o  27667  nosupbday  27677  nosupbnd2  27688  noinfbday  27692  noinfbnd2  27703  noetasuplem4  27708  noetainflem4  27712  noetalem1  27713  conway  27777  slerec  27797  sltlpss  27890  addsprop  27958  bdayon  28257  n0sfincut  28335  eucliddivs  28355  remulscllem2  28480  tgjustc1  28530  tgjustc2  28531  legov  28640  legtrid  28646  tglinethru  28691  tglnpt2  28696  tglineintmo  28697  mirreu3  28709  perpcom  28768  colperpexlem3  28787  mideu  28793  opphllem1  28802  hlpasch  28811  lnopp2hpgb  28818  trgcopy  28859  brcgr  28956  brbtwn2  28961  colinearalg  28966  axsegcon  28983  axeuclidlem  29018  axcontlem9  29028  ecgrtg  29039  elntg  29040  eengtrkg  29042  upgr1eopALT  29173  usgredg4  29273  subuhgr  29342  subumgr  29344  usgr2wspthon  30024  clwlkclwwlkf1  30068  eupth2lems  30296  n4cyclfrgr  30349  vacn  30752  blocni  30863  ubthlem3  30930  minvecolem7  30941  chocunii  31359  pjhthmo  31360  pjhthlem2  31450  kbass5  32178  mdsymlem5  32465  foresf1o  32561  fcobij  32780  xrofsup  32828  mgcoval  33049  mgcf1o  33066  xrge0tsmsd  33136  symgcntz  33148  archirngz  33252  archiabllem2a  33257  isarchiofld  33262  prmidl2  33503  mplvrpmmhm  33692  constrelextdg2  33885  smatrcl  33934  reff  33977  ordtconnlem1  34062  qqhval2  34120  volmeas  34369  fiunelcarsg  34454  ballotlemfc0  34631  ballotlemfcc  34632  signstfvneq0  34710  derangenlem  35346  erdsze2lem1  35378  pconnconn  35406  connpconn  35410  cvxsconn  35418  cvmliftmolem2  35457  cvmliftmo  35459  cvmlift2lem10  35487  cvmlift2lem12  35489  cvmlift3lem7  35500  mrsubff1  35689  msubff1  35731  r1peuqusdeg1  35818  ifscgr  36219  cgrxfr  36230  btwnconn1lem13  36274  btwnconn1lem14  36275  outsideofeq  36305  ellines  36327  finminlem  36493  fnejoin2  36544  weiunso  36641  unbdqndv2  36686  irrdiff  37502  poimirlem13  37805  poimirlem14  37806  poimirlem32  37824  opnmbllem0  37828  mblfinlem3  37831  itg2addnclem  37843  itg2addnc  37846  ftc1cnnc  37864  upixp  37901  filbcmb  37912  sstotbnd2  37946  isbnd3  37956  prdsbnd2  37967  cntotbnd  37968  ismtyima  37975  bfp  37996  rrncmslem  38004  unichnidl  38203  lshpcmp  39285  islshpat  39314  lfl0f  39366  ishlat3N  39651  3dim1  39764  islvol5  39876  lvoli2  39878  lncvrelatN  40078  pclfinclN  40247  pexmidlem8N  40274  idltrn  40447  cdleme42keg  40783  cdleme42mgN  40785  cdlemf2  40859  cdlemg2cex  40888  trlcoat  41020  dihopelvalcpre  41545  dih1dimatlem  41626  dihjatcclem4  41718  lcfl7N  41798  lcfrlem9  41847  mapdh9a  42086  hdmapglem7  42226  aks4d1p8  42378  isprimroot  42384  evl1gprodd  42408  sticksstones11  42447  grpods  42485  aks5lem8  42492  renegeulemv  42659  sn-subeu  42718  remulinvcom  42724  imacrhmcl  42805  fidomncyc  42826  fsuppind  42869  fsuppssind  42872  mhpind  42873  prjspertr  42884  prjspreln0  42888  flt4lem7  42938  nna4b4nsq  42939  nacsfix  42990  mzpsubst  43026  mzpcompact2lem  43029  eldioph2lem2  43039  eldioph2  43040  eldioph2b  43041  diophin  43050  diophun  43051  irrapxlem3  43102  irrapxlem5  43104  pell1234qrreccl  43132  pell1234qrmulcl  43133  pell14qrdich  43147  pell1qrge1  43148  pell1qrgaplem  43151  monotuz  43219  acongtr  43256  acongrep  43258  jm2.23  43274  jm2.26a  43278  jm2.26lem3  43279  jm2.26  43280  jm2.27  43286  wepwsolem  43320  fnwe2lem2  43329  kelac1  43341  kercvrlsm  43361  hbtlem5  43406  hbt  43408  mpaaeu  43428  cantnfresb  43602  onmcl  43609  tfsconcatun  43615  tfsconcatfn  43616  tfsconcatfv1  43617  tfsconcatfv2  43618  naddcnff  43640  rfovcnvf1od  44281  mnurndlem1  44558  cncmpmax  45313  rfcnnnub  45317  disjxp1  45350  iccintsng  45805  fprodcn  45882  lptioo2  45913  lptioo1  45914  limclner  45931  stoweidlem31  46311  stoweidlem34  46314  stoweidlem35  46315  stoweidlem49  46329  stoweidlem59  46339  stoweidlem62  46342  fourierdlem60  46446  fourierdlem61  46447  fourierdlem87  46473  iundjiun  46740  ismeannd  46747  hoidmvle  46880  smfsuplem2  47092  2reu8i  47395  prproropf1olem2  47786  paireqne  47793  perfectALTVlem2  48004  mogoldbb  48067  bgoldbtbndlem2  48088  bgoldbtbndlem3  48089  grimedg  48217  grlimprclnbgrvtx  48281  scmsuppss  48653  lindslinindsimp2lem5  48744  elfzolborelfzop1  48801  elbigolo1  48839  itschlc0xyqsol1  49048  itschlc0xyqsol  49049  iccdisj  49179  toslat  49263  iinfssclem3  49337  iinfssc  49338  iinfsubc  49339  imasubc3  49437  upciclem4  49450  uppropd  49462  natoppf  49510  tposcurf1  49580  fuco22  49620  fuco22natlem  49626  functhinclem4  49728  arweuthinc  49810