Theorem simplrr 789

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5105  frpomin  6341  fsnex  7281  f1prex  7282  isotr  7334  weniso  7352  riota5f  7395  frxp2  8139  frxp3  8146  xpord3pred  8147  poseq  8153  fprlem2  8297  tfrlem9a  8372  oaass  8545  oeeui  8587  oaabs2  8634  coflton  8656  cofon1  8657  naddssim  8671  resixpfo  8933  omxpenlem  9065  pw2f1olem  9068  fopwdom  9072  fofinf1o  9288  marypha1lem  9392  ordiso2  9476  oismo  9501  ixpiunwdom  9551  cantnf  9661  ttrclss  9688  fseqenlem1  10007  iunfictbso  10097  dfac12lem2  10127  dfac12lem3  10128  infunsdom1  10194  infpssrlem5  10290  fin23lem24  10305  isf32lem2  10337  isf32lem4  10339  isf34lem4  10360  fin1a2lem12  10394  fin1a2lem13  10395  ttukeylem6  10497  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  winalim2  10680  wunex2  10722  tskord  10764  prlem934  11017  mulcmpblnr  11055  dedekind  11372  addrid  11389  cnegex  11390  negeu  11446  add20  11725  divdivdiv  11915  ltmul12a  12070  lemul12a  12072  lediv12a  12107  supaddc  12181  supmul1  12183  cru  12209  uzwo3  12966  xleadd1a  13278  xmullem  13289  xmulgt0  13308  xlemul1a  13313  ixxun  13387  ixxss12  13391  ioodisj  13508  fz0fzelfz0  13661  mulexpz  14137  rpexpmord  14203  leexp1a  14210  expmulnbnd  14270  hashf1  14493  fi1uzind  14543  brfi1indALT  14546  swrdccat  14771  reuccatpfxs1  14783  abs3lem  15389  rexanre  15397  cau3lem  15405  limsupgre  15531  limsupbnd2  15533  o1lo1  15587  rlimclim1  15595  rlimclim  15596  rlimcn1  15638  rlimcn3  15640  o1of2  15663  o1rlimmul  15669  lo1add  15677  lo1mul  15678  isercolllem1  15715  climcau  15721  caucvgrlem  15723  caucvgb  15730  summolem2  15766  summo  15767  modfsummod  15845  o1fsum  15864  prodmolem2  15988  addmodlteqALT  16382  rpdvds  16717  isprm5  16765  isprm6  16772  pclem  16897  pcqmul  16912  pcexp  16918  pcneg  16933  pcprmpw2  16941  pcadd  16948  pcmpt  16951  4sqlem13  17016  vdwlem2  17041  vdwlem7  17046  vdwlem12  17051  ramval  17067  ramub2  17073  ramz2  17083  ramcl  17088  cshwshashlem2  17155  imasval  17564  imasdsval  17568  mreexexd  17703  acsfn  17714  issubc3  17905  idfucl  17937  funcres2c  17959  isnat  18006  fucpropd  18036  xpcval  18232  xpcco  18238  prfval  18254  evlf2  18273  evlfcl  18277  curf12  18282  curf1cl  18283  curf2  18284  curfcl  18287  curf2ndf  18302  hof2val  18311  hofcl  18314  hofpropd  18322  yonedalem4a  18330  yonedainv  18336  drsdirfi  18360  pospo  18398  poslubmo  18464  posglbmo  18465  isipodrs  18592  acsinfd  18611  chnccat  18681  chnpof1  18685  gsumvalx  18733  gsumpropd2lem  18736  mgmhmeql  18773  sgrppropd  18788  ismndd  18813  mndpropd  18816  mndpsuppss  18822  mhmeql  18884  mndind  18886  frmdup3lem  18924  mhmmnd  19129  issubg4  19211  ssnmz  19231  conjnmzb  19322  f1otrspeq  19516  psgneu  19575  pgpfi  19674  sylow2blem3  19691  slwhash  19693  fislw  19694  sylow3lem2  19697  lsmdisj2  19751  pj1eu  19765  efgredlem  19816  frgpuplem  19841  gexex  19922  frgpnabl  19944  dprdfadd  20091  dpjidcl  20129  pgpfac1lem3  20148  pgpfaclem3  20154  ablfac2  20160  ablsimpgcygd  20177  ablsimpgfind  20181  ablsimpgprmd  20186  rngpropd  20251  ringpropd  20370  imadrhmcl  20879  islmhm2  21138  lmhmpropd  21173  lbsextlem4  21264  prmidl2  21445  prmirredlem  21601  psgndiflemA  21730  lsmcss  21821  uvcf1  21921  frlmsslsp  21925  frlmup1  21927  assapropd  22000  psrval  22044  evlslem1  22212  mamucl  22537  mamuass  22538  mamudi  22539  mamudir  22540  mamuvs1  22541  mamuvs2  22542  mamulid  22577  mamurid  22578  dmatsubcl  22634  dmatmulcl  22636  scmatscm  22649  marrepval  22698  marepveval  22704  mdetunilem7  22754  gsummatr01lem4  22794  cpmatmcllem  22854  mat2pmatf1  22865  mat2pmatlin  22871  decpmatmul  22908  pm2mpmhmlem2  22955  chpidmat  22983  pptbas  23144  toponmre  23229  restbas  23294  iscncl  23405  cnrest2  23422  cnpdis  23429  lmcnp  23440  dishaus  23518  cmpcovf  23527  tgcmp  23537  dfconn2  23555  clsconn  23566  2ndcctbss  23591  dis2ndc  23596  1stccnp  23598  islly2  23620  cldllycmp  23631  locfincmp  23662  comppfsc  23668  kgentopon  23674  txcls  23740  ptpjopn  23748  dfac14  23754  xkoccn  23755  txcnp  23756  txcmpb  23780  txlm  23784  xkopt  23791  xkoco1cn  23793  xkoco2cn  23794  qtopcn  23850  qtoprest  23853  regr1lem2  23876  xkocnv  23950  qtophmeo  23953  fmfnfmlem4  24093  hausflim  24117  hauspwpwf1  24123  fclscmp  24166  alexsublem  24180  alexsubALTlem2  24184  alexsubALTlem3  24185  ptcmplem3  24190  ptcmplem4  24191  ptcmplem5  24192  cnextfun  24200  tmdgsum2  24232  symgtgp  24242  tsmsval2  24266  tsmsgsum  24275  utoptop  24370  ismet2  24469  blin  24557  metss2lem  24647  methaus  24656  met1stc  24657  met2ndci  24658  prdsxmslem2  24665  metcnp3  24676  metcnpi3  24682  metustto  24689  metustfbas  24693  nlmvscn  24823  nrginvrcn  24828  xrsxmet  24946  reconnlem1  24963  reconn  24965  xrge0tsms  24971  xmetdcn2  24974  metdscn  24993  addcnlem  25001  fsumcn  25008  cnheiborlem  25092  cnheibor  25093  bndth  25096  lebnum  25102  nmoleub2lem2  25254  ipcn  25384  iscmet3  25431  caubl  25446  rrxdstprj1  25547  minveclem3b  25566  minveclem7  25573  pjthlem2  25576  pmltpc  25588  volfiniun  25685  ioombl1  25700  dyadss  25732  dyaddisjlem  25733  dyadmax  25736  dyadmbllem  25737  opnmbllem  25739  itg1addlem2  25835  itg10a  25848  mbfi1fseqlem6  25858  itg2seq  25880  itg2monolem1  25888  itg2gt0  25898  itgfsum  25965  limcfval  26010  ellimc2  26015  ellimc3  26017  limcres  26024  limciun  26032  dvres  26049  dveflem  26117  rolle  26128  dvlip2  26133  c1liplem1  26134  dvgt0lem1  26140  dvgt0  26142  dvlt0  26143  dvne0  26149  dvfsumrlimge0  26168  ftc1lem6  26179  itgsubst  26187  mdegmullem  26214  ply1domn  26260  ply1divex  26273  fta1g  26306  fta1b  26308  plyf  26334  dgrlem  26365  coeid  26374  plydivalg  26439  aannenlem1  26468  aalioulem3  26474  aalioulem6  26477  abelthlem8  26578  efif1olem4  26686  chordthm  26978  xrlimcnp  27109  jensen  27129  lgamcvglem  27180  lgamcvg2  27195  sqf11  27279  fsumvma2  27354  perfectlem2  27370  lgsdilem  27464  lgsquad2lem2  27525  lgsquad3  27527  2sqlem5  27562  2sqlem9  27567  2sqb  27572  rpvmasumlem  27627  dchrisum0flb  27650  dchrisum0  27660  pntpbnd  27728  pntibndlem3  27732  pntleml  27751  nolt02o  27835  nosupbday  27845  nosupbnd2  27856  noinfbday  27860  noinfbnd2  27871  noetasuplem4  27876  noetainflem4  27880  noetalem1  27881  conway  27948  lesrec  27968  ltslpss  28077  addsprop  28145  bdayons  28445  n0fincut  28524  eucliddivs  28545  remulscllem2  28670  tgjustc1  28720  tgjustc2  28721  legov  28830  legtrid  28836  tglinethru  28885  tglineintmo  28891  tglnpt2  28902  mirreu3  28907  perpcom  28968  colperpexlem3  28988  mideu  28994  opphllem1  29003  hlpasch  29013  lnopp2hpgb  29020  trgcopy  29088  brcgr  29216  brbtwn2  29221  colinearalg  29226  axsegcon  29243  axeuclidlem  29278  axcontlem9  29288  ecgrtg  29299  elntg  29300  eengtrkg  29302  upgr1eopALT  29433  usgredg4  29533  subuhgr  29602  subumgr  29604  usgr2wspthon  30283  clwlkclwwlkf1  30327  eupth2lems  30555  n4cyclfrgr  30608  vacn  31012  blocni  31123  ubthlem3  31190  minvecolem7  31201  chocunii  31619  pjhthmo  31620  pjhthlem2  31710  kbass5  32438  mdsymlem5  32725  foresf1o  32816  fcobij  33031  xrofsup  33078  mgcoval  33272  mgcf1o  33289  xrge0tsmsd  33359  symgcntz  33371  archirngz  33475  archiabllem2a  33480  isarchiofld  33485  mplvrpmmhm  33902  constrelextdg2  34103  smatrcl  34152  reff  34195  ordtconnlem1  34280  qqhval2  34338  volmeas  34587  fiunelcarsg  34672  ballotlemfc0  34849  ballotlemfcc  34850  signstfvneq0  34925  derangenlem  35617  erdsze2lem1  35649  pconnconn  35677  connpconn  35681  cvxsconn  35689  cvmliftmolem2  35728  cvmliftmo  35730  cvmlift2lem10  35758  cvmlift2lem12  35760  cvmlift3lem7  35771  mrsubff1  35960  msubff1  36002  r1peuqusdeg1  36089  ifscgr  36490  cgrxfr  36501  btwnconn1lem13  36545  btwnconn1lem14  36546  outsideofeq  36576  ellines  36598  finminlem  36773  fnejoin2  36824  weiunso  36921  unbdqndv2  37044  irrdiff  37914  qdiff  37915  poimirlem13  38228  poimirlem14  38229  poimirlem32  38247  opnmbllem0  38251  mblfinlem3  38254  itg2addnclem  38266  itg2addnc  38269  ftc1cnnc  38287  upixp  38324  filbcmb  38335  sstotbnd2  38369  isbnd3  38379  prdsbnd2  38390  cntotbnd  38391  ismtyima  38398  bfp  38419  rrncmslem  38427  unichnidl  38626  lshpcmp  39708  islshpat  39737  lfl0f  39789  ishlat3N  40074  3dim1  40187  islvol5  40299  lvoli2  40301  lncvrelatN  40501  pclfinclN  40670  pexmidlem8N  40697  idltrn  40870  cdleme42keg  41206  cdleme42mgN  41208  cdlemf2  41282  cdlemg2cex  41311  trlcoat  41443  dihopelvalcpre  41968  dih1dimatlem  42049  dihjatcclem4  42141  lcfl7N  42221  lcfrlem9  42270  mapdh9a  42509  hdmapglem7  42649  aks4d1p8  42800  isprimroot  42806  evl1gprodd  42830  sticksstones11  42869  grpods  42907  aks5lem8  42914  renegeulemv  43075  sn-subeu  43134  remulinvcom  43140  imacrhmcl  43234  fidomncyc  43251  fsuppind  43270  fsuppssind  43273  mhpind  43274  prjspertr  43285  prjspreln0  43289  flt4lem7  43339  nna4b4nsq  43340  nacsfix  43391  mzpsubst  43427  mzpcompact2lem  43430  eldioph2lem2  43440  eldioph2  43441  eldioph2b  43442  diophin  43451  diophun  43452  irrapxlem3  43499  irrapxlem5  43501  pell1234qrreccl  43529  pell1234qrmulcl  43530  pell14qrdich  43544  pell1qrge1  43545  pell1qrgaplem  43548  monotuz  43616  acongtr  43653  acongrep  43655  jm2.23  43671  jm2.26a  43675  jm2.26lem3  43676  jm2.26  43677  jm2.27  43683  wepwsolem  43717  fnwe2lem2  43726  kelac1  43738  kercvrlsm  43758  hbtlem5  43803  hbt  43805  mpaaeu  43825  cantnfresb  43999  onmcl  44006  tfsconcatun  44012  tfsconcatfn  44013  tfsconcatfv1  44014  tfsconcatfv2  44015  naddcnff  44037  rfovcnvf1od  44678  mnurndlem1  44939  cncmpmax  45700  rfcnnnub  45704  disjxp1  45737  iccintsng  46187  fprodcn  46264  lptioo2  46295  lptioo1  46296  limclner  46313  stoweidlem31  46693  stoweidlem34  46696  stoweidlem35  46697  stoweidlem49  46711  stoweidlem59  46721  stoweidlem62  46724  fourierdlem60  46828  fourierdlem61  46829  fourierdlem87  46855  iundjiun  47122  ismeannd  47129  hoidmvle  47262  smfsuplem2  47474  2reu8i  47795  prproropf1olem2  48198  paireqne  48205  nprmmul2  48222  perfectALTVlem2  48432  mogoldbb  48495  bgoldbtbndlem2  48516  bgoldbtbndlem3  48517  grimedg  48645  grlimprclnbgrvtx  48709  scmsuppss  49096  lindslinindsimp2lem5  49187  elfzolborelfzop1  49244  elbigolo1  49282  itschlc0xyqsol1  49491  itschlc0xyqsol  49492  iccdisj  49621  toslat  49705  iinfssclem3  49779  iinfssc  49780  iinfsubc  49781  imasubc3  49879  upciclem4  49892  uppropd  49904  natoppf  49952  tposcurf1  50022  fuco22  50062  fuco22natlem  50068  functhinclem4  50170  arweuthinc  50252