Theorem simplrr 777

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  5086  frpomin  6283  fsnex  7212  f1prex  7213  isotr  7265  weniso  7283  riota5f  7326  frxp2  8069  frxp3  8076  xpord3pred  8077  poseq  8083  fprlem2  8226  tfrlem9a  8300  oaass  8471  oeeui  8512  oaabs2  8559  coflton  8581  cofon1  8582  naddssim  8595  resixpfo  8855  omxpenlem  8986  pw2f1olem  8989  fopwdom  8993  fofinf1o  9211  marypha1lem  9312  ordiso2  9396  oismo  9421  ixpiunwdom  9471  cantnf  9578  ttrclss  9605  fseqenlem1  9907  iunfictbso  9997  dfac12lem2  10028  dfac12lem3  10029  infunsdom1  10095  infpssrlem5  10190  fin23lem24  10205  isf32lem2  10237  isf32lem4  10239  isf34lem4  10260  fin1a2lem12  10294  fin1a2lem13  10295  ttukeylem6  10397  fpwwe2lem11  10524  fpwwe2lem12  10525  fpwwe2  10526  winalim2  10579  wunex2  10621  tskord  10663  prlem934  10916  mulcmpblnr  10954  dedekind  11268  addrid  11285  cnegex  11286  negeu  11342  add20  11621  divdivdiv  11814  ltmul12a  11969  lemul12a  11971  lediv12a  12007  supaddc  12081  supmul1  12083  cru  12109  uzwo3  12833  xleadd1a  13144  xmullem  13155  xmulgt0  13174  xlemul1a  13179  ixxun  13253  ixxss12  13257  ioodisj  13374  fz0fzelfz0  13526  mulexpz  14001  rpexpmord  14067  leexp1a  14074  expmulnbnd  14134  hashf1  14356  fi1uzind  14406  brfi1indALT  14409  swrdccat  14634  reuccatpfxs1  14646  abs3lem  15238  rexanre  15246  cau3lem  15254  limsupgre  15380  limsupbnd2  15382  o1lo1  15436  rlimclim1  15444  rlimclim  15445  rlimcn1  15487  rlimcn3  15489  o1of2  15512  o1rlimmul  15518  lo1add  15526  lo1mul  15527  isercolllem1  15564  climcau  15570  caucvgrlem  15572  caucvgb  15579  summolem2  15615  summo  15616  modfsummod  15693  o1fsum  15712  prodmolem2  15834  addmodlteqALT  16228  rpdvds  16563  isprm5  16610  isprm6  16617  pclem  16742  pcqmul  16757  pcexp  16763  pcneg  16778  pcprmpw2  16786  pcadd  16793  pcmpt  16796  4sqlem13  16861  vdwlem2  16886  vdwlem7  16891  vdwlem12  16896  ramval  16912  ramub2  16918  ramz2  16928  ramcl  16933  cshwshashlem2  17000  imasval  17407  imasdsval  17411  mreexexd  17546  acsfn  17557  issubc3  17748  idfucl  17780  funcres2c  17802  isnat  17849  fucpropd  17879  xpcval  18075  xpcco  18081  prfval  18097  evlf2  18116  evlfcl  18120  curf12  18125  curf1cl  18126  curf2  18127  curfcl  18130  curf2ndf  18145  hof2val  18154  hofcl  18157  hofpropd  18165  yonedalem4a  18173  yonedainv  18179  drsdirfi  18203  pospo  18241  poslubmo  18307  posglbmo  18308  isipodrs  18435  acsinfd  18454  chnccat  18524  chnpof1  18528  gsumvalx  18576  gsumpropd2lem  18579  mgmhmeql  18616  sgrppropd  18631  ismndd  18656  mndpropd  18659  mndpsuppss  18665  mhmeql  18726  mndind  18728  frmdup3lem  18766  mhmmnd  18969  issubg4  19050  ssnmz  19071  conjnmzb  19158  f1otrspeq  19352  psgneu  19411  pgpfi  19510  sylow2blem3  19527  slwhash  19529  fislw  19530  sylow3lem2  19533  lsmdisj2  19587  pj1eu  19601  efgredlem  19652  frgpuplem  19677  gexex  19758  frgpnabl  19780  dprdfadd  19927  dpjidcl  19965  pgpfac1lem3  19984  pgpfaclem3  19990  ablfac2  19996  ablsimpgcygd  20013  ablsimpgfind  20017  ablsimpgprmd  20022  rngpropd  20085  ringpropd  20199  imadrhmcl  20705  islmhm2  20965  lmhmpropd  21000  lbsextlem4  21091  prmirredlem  21402  psgndiflemA  21531  lsmcss  21622  uvcf1  21722  frlmsslsp  21726  frlmup1  21728  assapropd  21802  psrval  21845  evlslem1  22010  mamucl  22309  mamuass  22310  mamudi  22311  mamudir  22312  mamuvs1  22313  mamuvs2  22314  mamulid  22349  mamurid  22350  dmatsubcl  22406  dmatmulcl  22408  scmatscm  22421  marrepval  22470  marepveval  22476  mdetunilem7  22526  gsummatr01lem4  22566  cpmatmcllem  22626  mat2pmatf1  22637  mat2pmatlin  22643  decpmatmul  22680  pm2mpmhmlem2  22727  chpidmat  22755  pptbas  22916  toponmre  23001  restbas  23066  iscncl  23177  cnrest2  23194  cnpdis  23201  lmcnp  23212  dishaus  23290  cmpcovf  23299  tgcmp  23309  dfconn2  23327  clsconn  23338  2ndcctbss  23363  dis2ndc  23368  1stccnp  23370  islly2  23392  cldllycmp  23403  locfincmp  23434  comppfsc  23440  kgentopon  23446  txcls  23512  ptpjopn  23520  dfac14  23526  xkoccn  23527  txcnp  23528  txcmpb  23552  txlm  23556  xkopt  23563  xkoco1cn  23565  xkoco2cn  23566  qtopcn  23622  qtoprest  23625  regr1lem2  23648  xkocnv  23722  qtophmeo  23725  fmfnfmlem4  23865  hausflim  23889  hauspwpwf1  23895  fclscmp  23938  alexsublem  23952  alexsubALTlem2  23956  alexsubALTlem3  23957  ptcmplem3  23962  ptcmplem4  23963  ptcmplem5  23964  cnextfun  23972  tmdgsum2  24004  symgtgp  24014  tsmsval2  24038  tsmsgsum  24047  utoptop  24142  ismet2  24241  blin  24329  metss2lem  24419  methaus  24428  met1stc  24429  met2ndci  24430  prdsxmslem2  24437  metcnp3  24448  metcnpi3  24454  metustto  24461  metustfbas  24465  nlmvscn  24595  nrginvrcn  24600  xrsxmet  24718  reconnlem1  24735  reconn  24737  xrge0tsms  24743  xmetdcn2  24746  metdscn  24765  addcnlem  24773  fsumcn  24781  cnheiborlem  24873  cnheibor  24874  bndth  24877  lebnum  24883  nmoleub2lem2  25036  ipcn  25166  iscmet3  25213  caubl  25228  rrxdstprj1  25329  minveclem3b  25348  minveclem7  25355  pjthlem2  25358  pmltpc  25371  volfiniun  25468  ioombl1  25483  dyadss  25515  dyaddisjlem  25516  dyadmax  25519  dyadmbllem  25520  opnmbllem  25522  itg1addlem2  25618  itg10a  25631  mbfi1fseqlem6  25641  itg2seq  25663  itg2monolem1  25671  itg2gt0  25681  itgfsum  25748  limcfval  25793  ellimc2  25798  ellimc3  25800  limcres  25807  limciun  25815  dvres  25832  dveflem  25903  rolle  25914  dvlip2  25920  c1liplem1  25921  dvgt0lem1  25927  dvgt0  25929  dvlt0  25930  dvne0  25936  dvfsumrlimge0  25957  ftc1lem6  25968  itgsubst  25976  mdegmullem  26003  ply1domn  26049  ply1divex  26062  fta1g  26095  fta1b  26097  plyf  26123  dgrlem  26154  coeid  26163  plydivalg  26227  aannenlem1  26256  aalioulem3  26262  aalioulem6  26265  abelthlem8  26369  efif1olem4  26474  chordthm  26767  xrlimcnp  26898  jensen  26919  lgamcvglem  26970  lgamcvg2  26985  sqf11  27069  fsumvma2  27145  perfectlem2  27161  lgsdilem  27255  lgsquad2lem2  27316  lgsquad3  27318  2sqlem5  27353  2sqlem9  27358  2sqb  27363  rpvmasumlem  27418  dchrisum0flb  27441  dchrisum0  27451  pntpbnd  27519  pntibndlem3  27523  pntleml  27542  nolt02o  27627  nosupbday  27637  nosupbnd2  27648  noinfbday  27652  noinfbnd2  27663  noetasuplem4  27668  noetainflem4  27672  noetalem1  27673  conway  27733  slerec  27753  sltlpss  27846  addsprop  27912  bdayon  28202  n0sfincut  28275  eucliddivs  28294  remulscllem2  28396  tgjustc1  28446  tgjustc2  28447  legov  28556  legtrid  28562  tglinethru  28607  tglnpt2  28612  tglineintmo  28613  mirreu3  28625  perpcom  28684  colperpexlem3  28703  mideu  28709  opphllem1  28718  hlpasch  28727  lnopp2hpgb  28734  trgcopy  28775  brcgr  28871  brbtwn2  28876  colinearalg  28881  axsegcon  28898  axeuclidlem  28933  axcontlem9  28943  ecgrtg  28954  elntg  28955  eengtrkg  28957  upgr1eopALT  29088  usgredg4  29188  subuhgr  29257  subumgr  29259  usgr2wspthon  29936  clwlkclwwlkf1  29980  eupth2lems  30208  n4cyclfrgr  30261  vacn  30664  blocni  30775  ubthlem3  30842  minvecolem7  30853  chocunii  31271  pjhthmo  31272  pjhthlem2  31362  kbass5  32090  mdsymlem5  32377  foresf1o  32474  fcobij  32693  xrofsup  32740  mgcoval  32957  mgcf1o  32974  xrge0tsmsd  33032  symgcntz  33044  archirngz  33148  archiabllem2a  33153  isarchiofld  33158  prmidl2  33396  mplvrpmmhm  33566  constrelextdg2  33750  smatrcl  33799  reff  33842  ordtconnlem1  33927  qqhval2  33985  volmeas  34234  fiunelcarsg  34319  ballotlemfc0  34496  ballotlemfcc  34497  signstfvneq0  34575  derangenlem  35183  erdsze2lem1  35215  pconnconn  35243  connpconn  35247  cvxsconn  35255  cvmliftmolem2  35294  cvmliftmo  35296  cvmlift2lem10  35324  cvmlift2lem12  35326  cvmlift3lem7  35337  mrsubff1  35526  msubff1  35568  r1peuqusdeg1  35655  ifscgr  36057  cgrxfr  36068  btwnconn1lem13  36112  btwnconn1lem14  36113  outsideofeq  36143  ellines  36165  finminlem  36331  fnejoin2  36382  weiunso  36479  unbdqndv2  36524  irrdiff  37339  poimirlem13  37652  poimirlem14  37653  poimirlem32  37671  opnmbllem0  37675  mblfinlem3  37678  itg2addnclem  37690  itg2addnc  37693  ftc1cnnc  37711  upixp  37748  filbcmb  37759  sstotbnd2  37793  isbnd3  37803  prdsbnd2  37814  cntotbnd  37815  ismtyima  37822  bfp  37843  rrncmslem  37851  unichnidl  38050  lshpcmp  39006  islshpat  39035  lfl0f  39087  ishlat3N  39372  3dim1  39485  islvol5  39597  lvoli2  39599  lncvrelatN  39799  pclfinclN  39968  pexmidlem8N  39995  idltrn  40168  cdleme42keg  40504  cdleme42mgN  40506  cdlemf2  40580  cdlemg2cex  40609  trlcoat  40741  dihopelvalcpre  41266  dih1dimatlem  41347  dihjatcclem4  41439  lcfl7N  41519  lcfrlem9  41568  mapdh9a  41807  hdmapglem7  41947  aks4d1p8  42099  isprimroot  42105  evl1gprodd  42129  sticksstones11  42168  grpods  42206  aks5lem8  42213  renegeulemv  42380  sn-subeu  42439  remulinvcom  42445  imacrhmcl  42526  fidomncyc  42547  fsuppind  42602  fsuppssind  42605  mhpind  42606  prjspertr  42617  prjspreln0  42621  flt4lem7  42671  nna4b4nsq  42672  nacsfix  42724  mzpsubst  42760  mzpcompact2lem  42763  eldioph2lem2  42773  eldioph2  42774  eldioph2b  42775  diophin  42784  diophun  42785  irrapxlem3  42836  irrapxlem5  42838  pell1234qrreccl  42866  pell1234qrmulcl  42867  pell14qrdich  42881  pell1qrge1  42882  pell1qrgaplem  42885  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  43336  onmcl  43343  tfsconcatun  43349  tfsconcatfn  43350  tfsconcatfv1  43351  tfsconcatfv2  43352  naddcnff  43374  rfovcnvf1od  44016  mnurndlem1  44293  cncmpmax  45048  rfcnnnub  45052  disjxp1  45085  iccintsng  45542  fprodcn  45619  lptioo2  45650  lptioo1  45651  limclner  45668  stoweidlem31  46048  stoweidlem34  46051  stoweidlem35  46052  stoweidlem49  46066  stoweidlem59  46076  stoweidlem62  46079  fourierdlem60  46183  fourierdlem61  46184  fourierdlem87  46210  iundjiun  46477  ismeannd  46484  hoidmvle  46617  smfsuplem2  46829  2reu8i  47123  prproropf1olem2  47514  paireqne  47521  perfectALTVlem2  47732  mogoldbb  47795  bgoldbtbndlem2  47816  bgoldbtbndlem3  47817  grimedg  47945  grlimprclnbgrvtx  48009  scmsuppss  48381  lindslinindsimp2lem5  48473  elfzolborelfzop1  48530  elbigolo1  48568  itschlc0xyqsol1  48777  itschlc0xyqsol  48778  iccdisj  48908  toslat  48992  iinfssclem3  49067  iinfssc  49068  iinfsubc  49069  imasubc3  49167  upciclem4  49180  uppropd  49192  natoppf  49240  tposcurf1  49310  fuco22  49350  fuco22natlem  49356  functhinclem4  49458  arweuthinc  49540