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 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  disjxiun  5105  frpomin  6341  fsnex  7281  f1prex  7282  isotr  7334  weniso  7354  riota5f  7397  frxp2  8138  frxp3  8145  xpord3pred  8146  poseq  8152  fprlem2  8296  tfrlem9a  8371  oaass  8544  oeeui  8586  oaabs2  8633  coflton  8655  cofon1  8656  naddssim  8670  resixpfo  8932  omxpenlem  9064  pw2f1olem  9067  fopwdom  9071  fofinf1o  9287  marypha1lem  9391  ordiso2  9475  oismo  9500  ixpiunwdom  9550  cantnf  9660  ttrclss  9687  fseqenlem1  10015  iunfictbso  10105  dfac12lem2  10135  dfac12lem3  10136  infunsdom1  10202  infpssrlem5  10297  fin23lem24  10312  isf32lem2  10344  isf32lem4  10346  isf34lem4  10367  fin1a2lem12  10401  fin1a2lem13  10402  ttukeylem6  10504  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  winalim2  10687  wunex2  10729  tskord  10771  prlem934  11024  mulcmpblnr  11062  dedekind  11379  addrid  11396  cnegex  11397  negeu  11453  add20  11732  divdivdiv  11922  ltmul12a  12077  lemul12a  12079  lediv12a  12114  supaddc  12188  supmul1  12190  cru  12216  uzwo3  12973  xleadd1a  13285  xmullem  13296  xmulgt0  13315  xlemul1a  13320  ixxun  13394  ixxss12  13398  ioodisj  13515  fz0fzelfz0  13669  mulexpz  14145  rpexpmord  14211  leexp1a  14218  expmulnbnd  14278  hashf1  14501  fi1uzind  14551  brfi1indALT  14554  swrdccat  14779  reuccatpfxs1  14791  abs3lem  15397  rexanre  15405  cau3lem  15413  limsupgre  15539  limsupbnd2  15541  o1lo1  15595  rlimclim1  15603  rlimclim  15604  rlimcn1  15646  rlimcn3  15648  o1of2  15671  o1rlimmul  15677  lo1add  15685  lo1mul  15686  isercolllem1  15723  climcau  15729  caucvgrlem  15731  caucvgb  15738  summolem2  15774  summo  15775  modfsummod  15853  o1fsum  15872  prodmolem2  15996  addmodlteqALT  16389  rpdvds  16724  isprm5  16772  isprm6  16779  pclem  16904  pcqmul  16919  pcexp  16925  pcneg  16940  pcprmpw2  16948  pcadd  16955  pcmpt  16958  4sqlem13  17023  vdwlem2  17048  vdwlem7  17053  vdwlem12  17058  ramval  17074  ramub2  17080  ramz2  17090  ramcl  17095  cshwshashlem2  17162  imasval  17571  imasdsval  17575  mreexexd  17710  acsfn  17721  issubc3  17912  idfucl  17944  funcres2c  17966  isnat  18013  fucpropd  18043  xpcval  18239  xpcco  18245  prfval  18261  evlf2  18280  evlfcl  18284  curf12  18289  curf1cl  18290  curf2  18291  curfcl  18294  curf2ndf  18309  hof2val  18318  hofcl  18321  hofpropd  18329  yonedalem4a  18337  yonedainv  18343  drsdirfi  18367  pospo  18405  poslubmo  18471  posglbmo  18472  isipodrs  18599  acsinfd  18618  chnccat  18688  chnpof1  18692  gsumvalx  18740  gsumpropd2lem  18743  mgmhmeql  18780  sgrppropd  18795  ismndd  18820  mndpropd  18823  mndpsuppss  18829  mhmeql  18891  mndind  18893  frmdup3lem  18931  mhmmnd  19136  issubg4  19218  ssnmz  19238  conjnmzb  19329  f1otrspeq  19523  psgneu  19582  pgpfi  19681  sylow2blem3  19698  slwhash  19700  fislw  19701  sylow3lem2  19704  lsmdisj2  19758  pj1eu  19772  efgredlem  19823  frgpuplem  19848  gexex  19929  frgpnabl  19951  dprdfadd  20098  dpjidcl  20136  pgpfac1lem3  20155  pgpfaclem3  20161  ablfac2  20167  ablsimpgcygd  20184  ablsimpgfind  20188  ablsimpgprmd  20193  rngpropd  20258  ringpropd  20378  imadrhmcl  20911  islmhm2  21170  lmhmpropd  21205  lbsextlem4  21296  prmidl2  21477  prmirredlem  21633  psgndiflemA  21762  lsmcss  21853  uvcf1  21953  frlmsslsp  21957  frlmup1  21959  assapropd  22032  psrval  22076  evlslem1  22244  mamucl  22569  mamuass  22570  mamudi  22571  mamudir  22572  mamuvs1  22573  mamuvs2  22574  mamulid  22609  mamurid  22610  dmatsubcl  22666  dmatmulcl  22668  scmatscm  22681  marrepval  22730  marepveval  22736  mdetunilem7  22786  gsummatr01lem4  22826  cpmatmcllem  22886  mat2pmatf1  22897  mat2pmatlin  22903  decpmatmul  22940  pm2mpmhmlem2  22987  chpidmat  23015  pptbas  23176  toponmre  23261  restbas  23326  iscncl  23437  cnrest2  23454  cnpdis  23461  lmcnp  23472  dishaus  23550  cmpcovf  23559  tgcmp  23569  dfconn2  23587  clsconn  23598  2ndcctbss  23623  dis2ndc  23628  1stccnp  23630  islly2  23652  cldllycmp  23663  locfincmp  23694  comppfsc  23700  kgentopon  23706  txcls  23772  ptpjopn  23780  dfac14  23786  xkoccn  23787  txcnp  23788  txcmpb  23812  txlm  23816  xkopt  23823  xkoco1cn  23825  xkoco2cn  23826  qtopcn  23882  qtoprest  23885  regr1lem2  23908  xkocnv  23982  qtophmeo  23985  fmfnfmlem4  24125  hausflim  24149  hauspwpwf1  24155  fclscmp  24198  alexsublem  24212  alexsubALTlem2  24216  alexsubALTlem3  24217  ptcmplem3  24222  ptcmplem4  24223  ptcmplem5  24224  cnextfun  24232  tmdgsum2  24264  symgtgp  24274  tsmsval2  24298  tsmsgsum  24307  utoptop  24402  ismet2  24501  blin  24589  metss2lem  24679  methaus  24688  met1stc  24689  met2ndci  24690  prdsxmslem2  24697  metcnp3  24708  metcnpi3  24714  metustto  24721  metustfbas  24725  nlmvscn  24855  nrginvrcn  24860  xrsxmet  24978  reconnlem1  24995  reconn  24997  xrge0tsms  25003  xmetdcn2  25006  metdscn  25025  addcnlem  25033  fsumcn  25040  cnheiborlem  25124  cnheibor  25125  bndth  25128  lebnum  25134  nmoleub2lem2  25286  ipcn  25416  iscmet3  25463  caubl  25478  rrxdstprj1  25579  minveclem3b  25598  minveclem7  25605  pjthlem2  25608  pmltpc  25620  volfiniun  25717  ioombl1  25732  dyadss  25764  dyaddisjlem  25765  dyadmax  25768  dyadmbllem  25769  opnmbllem  25771  itg1addlem2  25867  itg10a  25880  mbfi1fseqlem6  25890  itg2seq  25912  itg2monolem1  25920  itg2gt0  25930  itgfsum  25997  limcfval  26042  ellimc2  26047  ellimc3  26049  limcres  26056  limciun  26064  dvres  26081  dveflem  26149  rolle  26160  dvlip2  26165  c1liplem1  26166  dvgt0lem1  26172  dvgt0  26174  dvlt0  26175  dvne0  26181  dvfsumrlimge0  26200  ftc1lem6  26211  itgsubst  26219  mdegmullem  26246  ply1domn  26292  ply1divex  26305  fta1g  26338  fta1b  26340  plyf  26366  dgrlem  26397  coeid  26406  plydivalg  26471  aannenlem1  26502  aalioulem3  26508  aalioulem6  26511  abelthlem8  26613  efif1olem4  26721  chordthm  27013  xrlimcnp  27144  jensen  27164  lgamcvglem  27215  lgamcvg2  27230  sqf11  27314  fsumvma2  27389  perfectlem2  27405  lgsdilem  27499  lgsquad2lem2  27560  lgsquad3  27562  2sqlem5  27597  2sqlem9  27602  2sqb  27607  rpvmasumlem  27662  dchrisum0flb  27685  dchrisum0  27695  pntpbnd  27763  pntibndlem3  27767  pntleml  27786  nolt02o  27870  nosupbday  27880  nosupbnd2  27891  noinfbday  27895  noinfbnd2  27906  noetasuplem4  27911  noetainflem4  27915  noetalem1  27916  conway  27983  lesrec  28003  ltslpss  28112  addsprop  28180  bdayons  28480  n0fincut  28559  eucliddivs  28580  remulscllem2  28705  tgjustc1  28755  tgjustc2  28756  legov  28865  legtrid  28871  tglinethru  28920  tglineintmo  28926  tglnpt2  28937  mirreu3  28942  perpcom  29004  colperpexlem3  29024  mideu  29030  opphllem1  29039  hlpasch  29049  lnopp2hpgb  29056  trgcopy  29126  brcgr  29261  brbtwn2  29266  colinearalg  29271  axsegcon  29288  axeuclidlem  29323  axcontlem9  29333  ecgrtg  29344  elntg  29345  eengtrkg  29347  upgr1eopALT  29478  usgredg4  29578  subuhgr  29647  subumgr  29649  usgr2wspthon  30328  clwlkclwwlkf1  30372  eupth2lems  30600  n4cyclfrgr  30653  vacn  31057  blocni  31168  ubthlem3  31235  minvecolem7  31246  chocunii  31664  pjhthmo  31665  pjhthlem2  31755  kbass5  32483  mdsymlem5  32770  foresf1o  32861  fcobij  33076  xrofsup  33123  mgcoval  33315  mgcf1o  33332  xrge0tsmsd  33402  symgcntz  33414  archirngz  33518  archiabllem2a  33523  isarchiofld  33528  mplvrpmmhm  33945  constrelextdg2  34146  smatrcl  34195  reff  34238  ordtconnlem1  34323  qqhval2  34381  volmeas  34630  fiunelcarsg  34715  ballotlemfc0  34892  ballotlemfcc  34893  signstfvneq0  34968  derangenlem  35671  erdsze2lem1  35703  pconnconn  35731  connpconn  35735  cvxsconn  35743  cvmliftmolem2  35782  cvmliftmo  35784  cvmlift2lem10  35812  cvmlift2lem12  35814  cvmlift3lem7  35825  mrsubff1  36014  msubff1  36056  r1peuqusdeg1  36143  ifscgr  36544  cgrxfr  36555  btwnconn1lem13  36599  btwnconn1lem14  36600  outsideofeq  36630  ellines  36652  nadddilem4  36723  finminlem  36857  fnejoin2  36908  weiunso  37005  unbdqndv2  37128  irrdiff  37998  qdiff  37999  poimirlem13  38312  poimirlem14  38313  poimirlem32  38331  opnmbllem0  38335  mblfinlem3  38338  itg2addnclem  38350  itg2addnc  38353  ftc1cnnc  38371  upixp  38408  filbcmb  38419  sstotbnd2  38453  isbnd3  38463  prdsbnd2  38474  cntotbnd  38475  ismtyima  38482  bfp  38503  rrncmslem  38511  unichnidl  38710  lshpcmp  39790  islshpat  39819  lfl0f  39871  ishlat3N  40156  3dim1  40269  islvol5  40381  lvoli2  40383  lncvrelatN  40583  pclfinclN  40752  pexmidlem8N  40779  idltrn  40952  cdleme42keg  41288  cdleme42mgN  41290  cdlemf2  41364  cdlemg2cex  41393  trlcoat  41525  dihopelvalcpre  42050  dih1dimatlem  42131  dihjatcclem4  42223  lcfl7N  42303  lcfrlem9  42352  mapdh9a  42591  hdmapglem7  42731  aks4d1p8  42882  isprimroot  42888  evl1gprodd  42912  sticksstones11  42951  grpods  42989  aks5lem8  42996  renegeulemv  43157  sn-subeu  43216  remulinvcom  43222  imacrhmcl  43316  fidomncyc  43331  fsuppind  43350  fsuppssind  43353  mhpind  43354  prjspertr  43365  prjspreln0  43369  flt4lem7  43419  nna4b4nsq  43420  nacsfix  43471  mzpsubst  43507  mzpcompact2lem  43510  eldioph2lem2  43520  eldioph2  43521  eldioph2b  43522  diophin  43531  diophun  43532  irrapxlem3  43579  irrapxlem5  43581  pell1234qrreccl  43609  pell1234qrmulcl  43610  pell14qrdich  43624  pell1qrge1  43625  pell1qrgaplem  43628  monotuz  43696  acongtr  43733  acongrep  43735  jm2.23  43751  jm2.26a  43755  jm2.26lem3  43756  jm2.26  43757  jm2.27  43763  wepwsolem  43797  fnwe2lem2  43806  kelac1  43818  kercvrlsm  43838  hbtlem5  43883  hbt  43885  mpaaeu  43905  cantnfresb  44079  onmcl  44086  tfsconcatun  44092  tfsconcatfn  44093  tfsconcatfv1  44094  tfsconcatfv2  44095  naddcnff  44117  rfovcnvf1od  44758  mnurndlem1  45019  cncmpmax  45780  rfcnnnub  45784  disjxp1  45817  iccintsng  46267  fprodcn  46344  lptioo2  46375  lptioo1  46376  limclner  46393  stoweidlem31  46773  stoweidlem34  46776  stoweidlem35  46777  stoweidlem49  46791  stoweidlem59  46801  stoweidlem62  46804  fourierdlem60  46908  fourierdlem61  46909  fourierdlem87  46935  iundjiun  47202  ismeannd  47209  hoidmvle  47342  smfsuplem2  47554  2reu8i  47878  prproropf1olem2  48281  paireqne  48288  nprmmul2  48305  perfectALTVlem2  48515  mogoldbb  48578  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  grimedg  48728  grlimprclnbgrvtx  48792  scmsuppss  49179  lindslinindsimp2lem5  49270  elfzolborelfzop1  49327  elbigolo1  49365  itschlc0xyqsol1  49574  itschlc0xyqsol  49575  iccdisj  49704  toslat  49788  iinfssclem3  49862  iinfssc  49863  iinfsubc  49864  imasubc3  49962  upciclem4  49975  uppropd  49987  natoppf  50035  tposcurf1  50105  fuco22  50145  fuco22natlem  50151  functhinclem4  50253  arweuthinc  50335