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 727	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  5140  frpomin  6361  fsnex  7303  f1prex  7304  isotr  7356  weniso  7374  riota5f  7416  frxp2  8169  frxp3  8176  xpord3pred  8177  poseq  8183  fprlem2  8326  tfrlem9a  8426  oaass  8599  oeeui  8640  oaabs2  8687  coflton  8709  cofon1  8710  naddssim  8723  resixpfo  8976  omxpenlem  9113  pw2f1olem  9116  fopwdom  9120  fofinf1o  9372  marypha1lem  9473  ordiso2  9555  oismo  9580  ixpiunwdom  9630  cantnf  9733  ttrclss  9760  fseqenlem1  10064  iunfictbso  10154  dfac12lem2  10185  dfac12lem3  10186  infunsdom1  10252  infpssrlem5  10347  fin23lem24  10362  isf32lem2  10394  isf32lem4  10396  isf34lem4  10417  fin1a2lem12  10451  fin1a2lem13  10452  ttukeylem6  10554  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  winalim2  10736  wunex2  10778  tskord  10820  prlem934  11073  mulcmpblnr  11111  dedekind  11424  addrid  11441  cnegex  11442  negeu  11498  add20  11775  divdivdiv  11968  ltmul12a  12123  lemul12a  12125  lediv12a  12161  supaddc  12235  supmul1  12237  cru  12258  uzwo3  12985  xleadd1a  13295  xmullem  13306  xmulgt0  13325  xlemul1a  13330  ixxun  13403  ixxss12  13407  ioodisj  13522  fz0fzelfz0  13674  mulexpz  14143  rpexpmord  14208  leexp1a  14215  expmulnbnd  14274  hashf1  14496  fi1uzind  14546  brfi1indALT  14549  swrdccat  14773  reuccatpfxs1  14785  abs3lem  15377  rexanre  15385  cau3lem  15393  limsupgre  15517  limsupbnd2  15519  o1lo1  15573  rlimclim1  15581  rlimclim  15582  rlimcn1  15624  rlimcn3  15626  o1of2  15649  o1rlimmul  15655  lo1add  15663  lo1mul  15664  isercolllem1  15701  climcau  15707  caucvgrlem  15709  caucvgb  15716  summolem2  15752  summo  15753  modfsummod  15830  o1fsum  15849  prodmolem2  15971  addmodlteqALT  16362  rpdvds  16697  isprm5  16744  isprm6  16751  pclem  16876  pcqmul  16891  pcexp  16897  pcneg  16912  pcprmpw2  16920  pcadd  16927  pcmpt  16930  4sqlem13  16995  vdwlem2  17020  vdwlem7  17025  vdwlem12  17030  ramval  17046  ramub2  17052  ramz2  17062  ramcl  17067  cshwshashlem2  17134  imasval  17556  imasdsval  17560  mreexexd  17691  acsfn  17702  issubc3  17894  idfucl  17926  funcres2c  17948  isnat  17995  fucpropd  18025  xpcval  18222  xpcco  18228  prfval  18244  evlf2  18263  evlfcl  18267  curf12  18272  curf1cl  18273  curf2  18274  curfcl  18277  curf2ndf  18292  hof2val  18301  hofcl  18304  hofpropd  18312  yonedalem4a  18320  yonedainv  18326  drsdirfi  18351  pospo  18390  poslubmo  18456  posglbmo  18457  isipodrs  18582  acsinfd  18601  gsumvalx  18689  gsumpropd2lem  18692  mgmhmeql  18729  sgrppropd  18744  ismndd  18769  mndpropd  18772  mndpsuppss  18778  mhmeql  18839  mndind  18841  frmdup3lem  18879  mhmmnd  19082  issubg4  19163  ssnmz  19184  conjnmzb  19271  f1otrspeq  19465  psgneu  19524  pgpfi  19623  sylow2blem3  19640  slwhash  19642  fislw  19643  sylow3lem2  19646  lsmdisj2  19700  pj1eu  19714  efgredlem  19765  frgpuplem  19790  gexex  19871  frgpnabl  19893  dprdfadd  20040  dpjidcl  20078  pgpfac1lem3  20097  pgpfaclem3  20103  ablfac2  20109  ablsimpgcygd  20126  ablsimpgfind  20130  ablsimpgprmd  20135  rngpropd  20171  ringpropd  20285  imadrhmcl  20798  islmhm2  21037  lmhmpropd  21072  lbsextlem4  21163  prmirredlem  21483  psgndiflemA  21619  lsmcss  21710  uvcf1  21812  frlmsslsp  21816  frlmup1  21818  assapropd  21892  psrval  21935  evlslem1  22106  mamucl  22405  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  mamulid  22447  mamurid  22448  dmatsubcl  22504  dmatmulcl  22506  scmatscm  22519  marrepval  22568  marepveval  22574  mdetunilem7  22624  gsummatr01lem4  22664  cpmatmcllem  22724  mat2pmatf1  22735  mat2pmatlin  22741  decpmatmul  22778  pm2mpmhmlem2  22825  chpidmat  22853  pptbas  23015  toponmre  23101  restbas  23166  iscncl  23277  cnrest2  23294  cnpdis  23301  lmcnp  23312  dishaus  23390  cmpcovf  23399  tgcmp  23409  dfconn2  23427  clsconn  23438  2ndcctbss  23463  dis2ndc  23468  1stccnp  23470  islly2  23492  cldllycmp  23503  locfincmp  23534  comppfsc  23540  kgentopon  23546  txcls  23612  ptpjopn  23620  dfac14  23626  xkoccn  23627  txcnp  23628  txcmpb  23652  txlm  23656  xkopt  23663  xkoco1cn  23665  xkoco2cn  23666  qtopcn  23722  qtoprest  23725  regr1lem2  23748  xkocnv  23822  qtophmeo  23825  fmfnfmlem4  23965  hausflim  23989  hauspwpwf1  23995  fclscmp  24038  alexsublem  24052  alexsubALTlem2  24056  alexsubALTlem3  24057  ptcmplem3  24062  ptcmplem4  24063  ptcmplem5  24064  cnextfun  24072  tmdgsum2  24104  symgtgp  24114  tsmsval2  24138  tsmsgsum  24147  utoptop  24243  ismet2  24343  blin  24431  metss2lem  24524  methaus  24533  met1stc  24534  met2ndci  24535  prdsxmslem2  24542  metcnp3  24553  metcnpi3  24559  metustto  24566  metustfbas  24570  nlmvscn  24708  nrginvrcn  24713  xrsxmet  24831  reconnlem1  24848  reconn  24850  xrge0tsms  24856  xmetdcn2  24859  metdscn  24878  addcnlem  24886  fsumcn  24894  cnheiborlem  24986  cnheibor  24987  bndth  24990  lebnum  24996  nmoleub2lem2  25149  ipcn  25280  iscmet3  25327  caubl  25342  rrxdstprj1  25443  minveclem3b  25462  minveclem7  25469  pjthlem2  25472  pmltpc  25485  volfiniun  25582  ioombl1  25597  dyadss  25629  dyaddisjlem  25630  dyadmax  25633  dyadmbllem  25634  opnmbllem  25636  itg1addlem2  25732  itg10a  25745  mbfi1fseqlem6  25755  itg2seq  25777  itg2monolem1  25785  itg2gt0  25795  itgfsum  25862  limcfval  25907  ellimc2  25912  ellimc3  25914  limcres  25921  limciun  25929  dvres  25946  dveflem  26017  rolle  26028  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  dvgt0  26043  dvlt0  26044  dvne0  26050  dvfsumrlimge0  26071  ftc1lem6  26082  itgsubst  26090  mdegmullem  26117  ply1domn  26163  ply1divex  26176  fta1g  26209  fta1b  26211  plyf  26237  dgrlem  26268  coeid  26277  plydivalg  26341  aannenlem1  26370  aalioulem3  26376  aalioulem6  26379  abelthlem8  26483  efif1olem4  26587  chordthm  26880  xrlimcnp  27011  jensen  27032  lgamcvglem  27083  lgamcvg2  27098  sqf11  27182  fsumvma2  27258  perfectlem2  27274  lgsdilem  27368  lgsquad2lem2  27429  lgsquad3  27431  2sqlem5  27466  2sqlem9  27471  2sqb  27476  rpvmasumlem  27531  dchrisum0flb  27554  dchrisum0  27564  pntpbnd  27632  pntibndlem3  27636  pntleml  27655  nolt02o  27740  nosupbday  27750  nosupbnd2  27761  noinfbday  27765  noinfbnd2  27776  noetasuplem4  27781  noetainflem4  27785  noetalem1  27786  conway  27844  slerec  27864  sltlpss  27945  addsprop  28009  remulscllem2  28433  tgjustc1  28483  tgjustc2  28484  legov  28593  legtrid  28599  tglinethru  28644  tglnpt2  28649  tglineintmo  28650  mirreu3  28662  perpcom  28721  colperpexlem3  28740  mideu  28746  opphllem1  28755  hlpasch  28764  lnopp2hpgb  28771  trgcopy  28812  brcgr  28915  brbtwn2  28920  colinearalg  28925  axsegcon  28942  axeuclidlem  28977  axcontlem9  28987  ecgrtg  28998  elntg  28999  eengtrkg  29001  upgr1eopALT  29134  usgredg4  29234  subuhgr  29303  subumgr  29305  usgr2wspthon  29985  clwlkclwwlkf1  30029  eupth2lems  30257  n4cyclfrgr  30310  vacn  30713  blocni  30824  ubthlem3  30891  minvecolem7  30902  chocunii  31320  pjhthmo  31321  pjhthlem2  31411  kbass5  32139  mdsymlem5  32426  foresf1o  32523  fcobij  32733  xrofsup  32771  mgcoval  32976  mgcf1o  32993  xrge0tsmsd  33065  symgcntz  33105  archirngz  33196  archiabllem2a  33201  isarchiofld  33347  prmidl2  33469  constrelextdg2  33788  smatrcl  33795  reff  33838  ordtconnlem1  33923  qqhval2  33983  volmeas  34232  fiunelcarsg  34318  ballotlemfc0  34495  ballotlemfcc  34496  signstfvneq0  34587  derangenlem  35176  erdsze2lem1  35208  pconnconn  35236  connpconn  35240  cvxsconn  35248  cvmliftmolem2  35287  cvmliftmo  35289  cvmlift2lem10  35317  cvmlift2lem12  35319  cvmlift3lem7  35330  mrsubff1  35519  msubff1  35561  r1peuqusdeg1  35648  ifscgr  36045  cgrxfr  36056  btwnconn1lem13  36100  btwnconn1lem14  36101  outsideofeq  36131  ellines  36153  finminlem  36319  fnejoin2  36370  weiunso  36467  unbdqndv2  36512  irrdiff  37327  poimirlem13  37640  poimirlem14  37641  poimirlem32  37659  opnmbllem0  37663  mblfinlem3  37666  itg2addnclem  37678  itg2addnc  37681  ftc1cnnc  37699  upixp  37736  filbcmb  37747  sstotbnd2  37781  isbnd3  37791  prdsbnd2  37802  cntotbnd  37803  ismtyima  37810  bfp  37831  rrncmslem  37839  unichnidl  38038  lshpcmp  38989  islshpat  39018  lfl0f  39070  ishlat3N  39355  3dim1  39469  islvol5  39581  lvoli2  39583  lncvrelatN  39783  pclfinclN  39952  pexmidlem8N  39979  idltrn  40152  cdleme42keg  40488  cdleme42mgN  40490  cdlemf2  40564  cdlemg2cex  40593  trlcoat  40725  dihopelvalcpre  41250  dih1dimatlem  41331  dihjatcclem4  41423  lcfl7N  41503  lcfrlem9  41552  mapdh9a  41791  hdmapglem7  41931  aks4d1p8  42088  isprimroot  42094  evl1gprodd  42118  sticksstones11  42157  grpods  42195  aks5lem8  42202  renegeulemv  42398  sn-subeu  42456  remulinvcom  42462  sn-itrere  42498  sn-retire  42499  imacrhmcl  42524  fidomncyc  42545  fsuppind  42600  fsuppssind  42603  mhpind  42604  prjspertr  42615  prjspreln0  42619  flt4lem7  42669  nna4b4nsq  42670  nacsfix  42723  mzpsubst  42759  mzpcompact2lem  42762  eldioph2lem2  42772  eldioph2  42773  eldioph2b  42774  diophin  42783  diophun  42784  irrapxlem3  42835  irrapxlem5  42837  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell14qrdich  42880  pell1qrge1  42881  pell1qrgaplem  42884  monotuz  42953  acongtr  42990  acongrep  42992  jm2.23  43008  jm2.26a  43012  jm2.26lem3  43013  jm2.26  43014  jm2.27  43020  wepwsolem  43054  fnwe2lem2  43063  kelac1  43075  kercvrlsm  43095  hbtlem5  43140  hbt  43142  mpaaeu  43162  cantnfresb  43337  onmcl  43344  tfsconcatun  43350  tfsconcatfn  43351  tfsconcatfv1  43352  tfsconcatfv2  43353  naddcnff  43375  rfovcnvf1od  44017  mnurndlem1  44300  cncmpmax  45037  rfcnnnub  45041  disjxp1  45074  iccintsng  45536  fprodcn  45615  lptioo2  45646  lptioo1  45647  limclner  45666  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem49  46064  stoweidlem59  46074  stoweidlem62  46077  fourierdlem60  46181  fourierdlem61  46182  fourierdlem87  46208  iundjiun  46475  ismeannd  46482  hoidmvle  46615  smfsuplem2  46827  2reu8i  47125  prproropf1olem2  47491  paireqne  47498  perfectALTVlem2  47709  mogoldbb  47772  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  uspgrimprop  47873  grimedg  47903  scmsuppss  48287  lindslinindsimp2lem5  48379  elfzolborelfzop1  48436  elbigolo1  48478  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  iccdisj  48796  toslat  48871  upciclem4  48926  tposcurf1  48999  fuco22  49034  fuco22natlem  49040  functhinclem4  49096