Theorem simplrr 790

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

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

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 402

This theorem is used by:  disjxiun  5099  frpomin  6332  fsnex  7279  f1prex  7280  isotr  7332  weniso  7352  riota5f  7393  frxp2  8139  frxp3  8146  xpord3pred  8147  poseq  8153  fprlem2  8297  tfrlem9a  8372  oaass  8547  oeeui  8589  oaabs2  8636  coflton  8658  cofon1  8659  naddssim  8673  resixpfo  8942  omxpenlem  9075  pw2f1olem  9078  fopwdom  9082  fofinf1o  9299  marypha1lem  9403  ordiso2  9487  oismo  9512  ixpiunwdom  9562  cantnf  9672  ttrclss  9699  fseqenlem1  10074  iunfictbso  10164  dfac12lem2  10194  dfac12lem3  10195  infunsdom1  10261  infpssrlem5  10356  fin23lem24  10371  isf32lem2  10403  isf32lem4  10405  isf34lem4  10426  fin1a2lem12  10460  fin1a2lem13  10461  ttukeylem6  10563  fpwwe2lem11  10697  fpwwe2lem12  10698  fpwwe2  10699  winalim2  10752  wunex2  10794  tskord  10836  prlem934  11089  mulcmpblnr  11127  dedekind  11444  addrid  11461  cnegex  11462  negeu  11518  add20  11797  divdivdiv  11987  ltmul12a  12142  lemul12a  12144  lediv12a  12179  supaddc  12253  supmul1  12255  cru  12281  uzwo3  13039  xleadd1a  13352  xmullem  13363  xmulgt0  13382  xlemul1a  13387  ixxun  13461  ixxss12  13465  ioodisj  13582  fz0fzelfz0  13736  mulexpz  14213  rpexpmord  14279  leexp1a  14286  expmulnbnd  14346  hashf1  14569  fi1uzind  14619  brfi1indALT  14622  swrdccat  14851  reuccatpfxs1  14863  abs3lem  15473  rexanre  15481  cau3lem  15489  limsupgre  15615  limsupbnd2  15617  o1lo1  15671  rlimclim1  15679  rlimclim  15680  rlimcn1  15722  rlimcn3  15724  o1of2  15747  o1rlimmul  15753  lo1add  15761  lo1mul  15762  isercolllem1  15799  climcau  15805  caucvgrlem  15807  caucvgb  15814  summolem2  15849  summo  15850  modfsummod  15928  o1fsum  15947  prodmolem2  16069  addmodlteqALT  16462  rpdvds  16797  isprm5  16845  isprm6  16852  pclem  16977  pcqmul  16992  pcexp  16998  pcneg  17013  pcprmpw2  17021  pcadd  17028  pcmpt  17031  4sqlem13  17096  vdwlem2  17121  vdwlem7  17126  vdwlem12  17131  ramval  17147  ramub2  17153  ramz2  17163  ramcl  17168  cshwshashlem2  17235  imasval  17644  imasdsval  17648  mreexexd  17783  acsfn  17794  issubc3  17985  idfucl  18017  funcres2c  18039  isnat  18086  fucpropd  18116  xpcval  18312  xpcco  18318  prfval  18334  evlf2  18353  evlfcl  18357  curf12  18362  curf1cl  18363  curf2  18364  curfcl  18367  curf2ndf  18382  hof2val  18391  hofcl  18394  hofpropd  18402  yonedalem4a  18410  yonedainv  18416  drsdirfi  18440  pospo  18478  poslubmo  18544  posglbmo  18545  isipodrs  18672  acsinfd  18691  chnccat  18761  chnpof1  18765  gsumvalx  18826  gsumpropd2lem  18829  mgmhmeql  18866  sgrppropd  18881  ismndd  18907  mndpropd  18912  mndpsuppss  18920  mhmeql  18983  mndind  18985  frmdup3lem  19023  mhmmnd  19235  issubg4  19317  ssnmz  19337  conjnmzb  19428  f1otrspeq  19622  psgneu  19681  pgpfi  19780  sylow2blem3  19797  slwhash  19799  fislw  19800  sylow3lem2  19803  lsmdisj2  19857  pj1eu  19871  efgredlem  19922  frgpuplem  19947  gexex  20028  frgpnabl  20050  dprdfadd  20197  dpjidcl  20235  pgpfac1lem3  20254  pgpfaclem3  20260  ablfac2  20266  ablsimpgcygd  20283  ablsimpgfind  20287  ablsimpgprmd  20292  rngpropd  20357  ringpropd  20480  imadrhmcl  21015  islmhm2  21274  lmhmpropd  21309  lbsextlem4  21400  prmidl2  21583  prmirredlem  21739  psgndiflemA  21868  lsmcss  21959  uvcf1  22059  frlmsslsp  22063  frlmup1  22065  assapropd  22140  psrval  22184  evlslem1  22352  mamucl  22677  mamuass  22678  mamudi  22679  mamudir  22680  mamuvs1  22681  mamuvs2  22682  mamulid  22717  mamurid  22718  dmatsubcl  22774  dmatmulcl  22776  scmatscm  22789  marrepval  22838  marepveval  22844  mdetunilem7  22894  gsummatr01lem4  22934  cpmatmcllem  22997  mat2pmatf1  23008  mat2pmatlin  23014  decpmatmul  23051  pm2mpmhmlem2  23098  chpidmat  23126  pptbas  23287  toponmre  23372  restbas  23437  iscncl  23548  cnrest2  23565  cnpdis  23572  lmcnp  23583  dishaus  23661  cmpcovf  23670  tgcmp  23680  dfconn2  23698  clsconn  23709  2ndcctbss  23735  dis2ndc  23740  1stccnp  23742  islly2  23764  cldllycmp  23775  locfincmp  23806  comppfsc  23812  kgentopon  23818  txcls  23884  ptpjopn  23892  dfac14  23898  xkoccn  23899  txcnp  23900  txcmpb  23924  txlm  23928  xkopt  23935  xkoco1cn  23937  xkoco2cn  23938  qtopcn  23994  qtoprest  23997  regr1lem2  24020  xkocnv  24094  qtophmeo  24097  fmfnfmlem4  24237  hausflim  24261  hauspwpwf1  24267  fclscmp  24310  alexsublem  24324  alexsubALTlem2  24328  alexsubALTlem3  24329  ptcmplem3  24334  ptcmplem4  24335  ptcmplem5  24336  cnextfun  24344  tmdgsum2  24376  symgtgp  24386  tsmsval2  24410  tsmsgsum  24419  utoptop  24514  ismet2  24613  blin  24701  metss2lem  24791  methaus  24800  met1stc  24801  met2ndci  24802  prdsxmslem2  24809  metcnp3  24820  metcnpi3  24826  metustto  24833  metustfbas  24837  nlmvscn  24967  nrginvrcn  24972  xrsxmet  25090  reconnlem1  25107  reconn  25109  xrge0tsms  25115  xmetdcn2  25118  metdscn  25137  addcnlem  25145  fsumcn  25152  cnheiborlem  25236  cnheibor  25237  bndth  25240  lebnum  25246  nmoleub2lem2  25398  ipcn  25528  iscmet3  25575  caubl  25590  rrxdstprj1  25691  minveclem3b  25710  minveclem7  25717  pjthlem2  25720  pmltpc  25732  volfiniun  25829  ioombl1  25844  dyadss  25876  dyaddisjlem  25877  dyadmax  25880  dyadmbllem  25881  opnmbllem  25883  itg1addlem2  25979  itg10a  25992  mbfi1fseqlem6  26002  itg2seq  26024  itg2monolem1  26032  itg2gt0  26042  itgfsum  26108  limcfval  26153  ellimc2  26158  ellimc3  26160  limcres  26167  limciun  26175  dvres  26192  dveflem  26260  rolle  26271  dvlip2  26276  c1liplem1  26277  dvgt0lem1  26283  dvgt0  26285  dvlt0  26286  dvne0  26292  dvfsumrlimge0  26311  ftc1lem6  26322  itgsubst  26330  mdegmullem  26357  ply1domn  26403  ply1divex  26416  fta1g  26449  fta1b  26451  plyf  26477  dgrlem  26509  coeid  26518  plydivalg  26583  aannenlem1  26618  aalioulem3  26624  aalioulem6  26627  abelthlem8  26729  efif1olem4  26836  chordthm  27128  xrlimcnp  27259  jensen  27279  lgamcvglem  27330  lgamcvg2  27345  sqf11  27429  fsumvma2  27504  perfectlem2  27520  lgsdilem  27614  lgsquad2lem2  27675  lgsquad3  27677  2sqlem5  27712  2sqlem9  27717  2sqb  27722  rpvmasumlem  27777  dchrisum0flb  27800  dchrisum0  27810  pntpbnd  27878  pntibndlem3  27882  pntleml  27901  nolt02o  27985  nosupbday  27995  nosupbnd2  28006  noinfbday  28010  noinfbnd2  28021  noetasuplem4  28026  noetainflem4  28030  noetalem1  28031  conway  28098  lesrec  28118  ltslpss  28227  addsprop  28295  bdayons  28595  n0fincut  28674  eucliddivs  28695  remulscllem2  28820  tgjustc1  28870  tgjustc2  28871  legov  28981  legtrid  28987  tglinethru  29037  tglineintmo  29043  tglnpt2  29054  mirreu3  29059  perpcom  29121  colperpexlem3  29141  mideu  29147  opphllem1  29156  hlpasch  29167  lnopp2hpgb  29174  trgcopy  29244  brcgr  29411  brbtwn2  29416  colinearalg  29421  axsegcon  29438  axeuclidlem  29473  axcontlem9  29483  ecgrtg  29494  elntg  29495  eengtrkg  29497  upgr1eopALT  29628  usgredg4  29731  subuhgr  29800  subumgr  29802  usgr2wspthon  30490  clwlkclwwlkf1  30534  eupth2lems  30772  n4cyclfrgr  30825  vacn  31229  blocni  31340  ubthlem3  31407  minvecolem7  31418  chocunii  31836  pjhthmo  31837  pjhthlem2  31927  kbass5  32655  mdsymlem5  32942  foresf1o  33033  fcobij  33245  xrofsup  33292  mgcoval  33480  mgcf1o  33497  xrge0tsmsd  33567  symgcntz  33579  archirngz  33683  archiabllem2a  33688  isarchiofld  33693  mplvrpmmhm  34111  constrelextdg2  34312  smatrcl  34361  reff  34404  ordtconnlem1  34489  qqhval2  34547  volmeas  34797  fiunelcarsg  34882  ballotlemfc0  35059  ballotlemfcc  35060  signstfvneq0  35135  derangenlem  35857  erdsze2lem1  35889  pconnconn  35917  connpconn  35921  cvxsconn  35929  cvmliftmolem2  35968  cvmliftmo  35970  cvmlift2lem10  35998  cvmlift2lem12  36000  cvmlift3lem7  36011  mrsubff1  36200  msubff1  36242  r1peuqusdeg1  36329  ifscgr  36731  cgrxfr  36742  btwnconn1lem13  36786  btwnconn1lem14  36787  outsideofeq  36817  ellines  36839  nadddilem4  36894  finminlem  37028  fnejoin2  37079  weiunso  37176  unbdqndv2  37299  irrdiff  38167  qdiff  38168  poimirlem13  38471  poimirlem14  38472  poimirlem32  38490  opnmbllem0  38494  mblfinlem3  38497  itg2addnclem  38509  itg2addnc  38512  ftc1cnnc  38530  upixp  38583  filbcmb  38594  sstotbnd2  38628  isbnd3  38638  prdsbnd2  38649  cntotbnd  38650  ismtyima  38657  bfp  38678  rrncmslem  38686  unichnidl  38885  lshpcmp  39965  islshpat  39994  lfl0f  40046  ishlat3N  40331  3dim1  40444  islvol5  40556  lvoli2  40558  lncvrelatN  40758  pclfinclN  40927  pexmidlem8N  40954  idltrn  41127  cdleme42keg  41463  cdleme42mgN  41465  cdlemf2  41539  cdlemg2cex  41568  trlcoat  41700  dihopelvalcpre  42225  dih1dimatlem  42306  dihjatcclem4  42398  lcfl7N  42478  lcfrlem9  42527  mapdh9a  42766  hdmapglem7  42906  aks4d1p8  43057  isprimroot  43063  evl1gprodd  43087  sticksstones11  43126  grpods  43164  aks5lem8  43171  renegeulemv  43347  sn-subeu  43406  remulinvcom  43412  imacrhmcl  43506  fidomncyc  43521  fsuppind  43540  fsuppssind  43543  mhpind  43544  prjspertr  43555  prjspreln0  43559  flt4lem7  43609  nna4b4nsq  43610  nacsfix  43661  mzpsubst  43697  mzpcompact2lem  43700  eldioph2lem2  43710  eldioph2  43711  eldioph2b  43712  diophin  43721  diophun  43722  irrapxlem3  43769  irrapxlem5  43771  pell1234qrreccl  43799  pell1234qrmulcl  43800  pell14qrdich  43814  pell1qrge1  43815  pell1qrgaplem  43818  monotuz  43886  acongtr  43923  acongrep  43925  jm2.23  43941  jm2.26a  43945  jm2.26lem3  43946  jm2.26  43947  jm2.27  43953  wepwsolem  43987  fnwe2lem2  43996  kelac1  44008  kercvrlsm  44028  hbtlem5  44073  hbt  44075  mpaaeu  44095  cantnfresb  44269  onmcl  44276  tfsconcatun  44282  tfsconcatfn  44283  tfsconcatfv1  44284  tfsconcatfv2  44285  naddcnff  44307  rfovcnvf1od  44948  mnurndlem1  45209  cncmpmax  45970  rfcnnnub  45974  disjxp1  46007  iccintsng  46457  fprodcn  46534  lptioo2  46565  lptioo1  46566  limclner  46583  stoweidlem31  46963  stoweidlem34  46966  stoweidlem35  46967  stoweidlem49  46981  stoweidlem59  46991  stoweidlem62  46994  fourierdlem60  47098  fourierdlem61  47099  fourierdlem87  47125  iundjiun  47392  ismeannd  47399  hoidmvle  47532  smfsuplem2  47744  2reu8i  48105  prproropf1olem2  48508  paireqne  48515  nprmmul2  48532  perfectALTVlem2  48742  mogoldbb  48805  bgoldbtbndlem2  48826  bgoldbtbndlem3  48827  grimedg  48955  grlimprclnbgrvtx  49019  scmsuppss  49405  lindslinindsimp2lem5  49496  elfzolborelfzop1  49553  elbigolo1  49591  itschlc0xyqsol1  49800  itschlc0xyqsol  49801  iccdisj  49928  toslat  50012  iinfssclem3  50086  iinfssc  50087  iinfsubc  50088  imasubc3  50186  upciclem4  50199  uppropd  50211  natoppf  50259  tposcurf1  50329  fuco22  50369  fuco22natlem  50375  functhinclem4  50477  arweuthinc  50559