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 728	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  5096  frpomin  6299  fsnex  7232  f1prex  7233  isotr  7285  weniso  7303  riota5f  7346  frxp2  8089  frxp3  8096  xpord3pred  8097  poseq  8103  fprlem2  8246  tfrlem9a  8320  oaass  8491  oeeui  8533  oaabs2  8580  coflton  8602  cofon1  8603  naddssim  8616  resixpfo  8879  omxpenlem  9011  pw2f1olem  9014  fopwdom  9018  fofinf1o  9237  marypha1lem  9341  ordiso2  9425  oismo  9450  ixpiunwdom  9500  cantnf  9607  ttrclss  9634  fseqenlem1  9939  iunfictbso  10029  dfac12lem2  10060  dfac12lem3  10061  infunsdom1  10127  infpssrlem5  10222  fin23lem24  10237  isf32lem2  10269  isf32lem4  10271  isf34lem4  10292  fin1a2lem12  10326  fin1a2lem13  10327  ttukeylem6  10429  fpwwe2lem11  10557  fpwwe2lem12  10558  fpwwe2  10559  winalim2  10612  wunex2  10654  tskord  10696  prlem934  10949  mulcmpblnr  10987  dedekind  11301  addrid  11318  cnegex  11319  negeu  11375  add20  11654  divdivdiv  11847  ltmul12a  12002  lemul12a  12004  lediv12a  12040  supaddc  12114  supmul1  12116  cru  12142  uzwo3  12861  xleadd1a  13173  xmullem  13184  xmulgt0  13203  xlemul1a  13208  ixxun  13282  ixxss12  13286  ioodisj  13403  fz0fzelfz0  13555  mulexpz  14030  rpexpmord  14096  leexp1a  14103  expmulnbnd  14163  hashf1  14385  fi1uzind  14435  brfi1indALT  14438  swrdccat  14663  reuccatpfxs1  14675  abs3lem  15267  rexanre  15275  cau3lem  15283  limsupgre  15409  limsupbnd2  15411  o1lo1  15465  rlimclim1  15473  rlimclim  15474  rlimcn1  15516  rlimcn3  15518  o1of2  15541  o1rlimmul  15547  lo1add  15555  lo1mul  15556  isercolllem1  15593  climcau  15599  caucvgrlem  15601  caucvgb  15608  summolem2  15644  summo  15645  modfsummod  15722  o1fsum  15741  prodmolem2  15863  addmodlteqALT  16257  rpdvds  16592  isprm5  16639  isprm6  16646  pclem  16771  pcqmul  16786  pcexp  16792  pcneg  16807  pcprmpw2  16815  pcadd  16822  pcmpt  16825  4sqlem13  16890  vdwlem2  16915  vdwlem7  16920  vdwlem12  16925  ramval  16941  ramub2  16947  ramz2  16957  ramcl  16962  cshwshashlem2  17029  imasval  17437  imasdsval  17441  mreexexd  17576  acsfn  17587  issubc3  17778  idfucl  17810  funcres2c  17832  isnat  17879  fucpropd  17909  xpcval  18105  xpcco  18111  prfval  18127  evlf2  18146  evlfcl  18150  curf12  18155  curf1cl  18156  curf2  18157  curfcl  18160  curf2ndf  18175  hof2val  18184  hofcl  18187  hofpropd  18195  yonedalem4a  18203  yonedainv  18209  drsdirfi  18233  pospo  18271  poslubmo  18337  posglbmo  18338  isipodrs  18465  acsinfd  18484  chnccat  18554  chnpof1  18558  gsumvalx  18606  gsumpropd2lem  18609  mgmhmeql  18646  sgrppropd  18661  ismndd  18686  mndpropd  18689  mndpsuppss  18695  mhmeql  18756  mndind  18758  frmdup3lem  18796  mhmmnd  18999  issubg4  19080  ssnmz  19100  conjnmzb  19187  f1otrspeq  19381  psgneu  19440  pgpfi  19539  sylow2blem3  19556  slwhash  19558  fislw  19559  sylow3lem2  19562  lsmdisj2  19616  pj1eu  19630  efgredlem  19681  frgpuplem  19706  gexex  19787  frgpnabl  19809  dprdfadd  19956  dpjidcl  19994  pgpfac1lem3  20013  pgpfaclem3  20019  ablfac2  20025  ablsimpgcygd  20042  ablsimpgfind  20046  ablsimpgprmd  20051  rngpropd  20114  ringpropd  20228  imadrhmcl  20735  islmhm2  20995  lmhmpropd  21030  lbsextlem4  21121  prmirredlem  21432  psgndiflemA  21561  lsmcss  21652  uvcf1  21752  frlmsslsp  21756  frlmup1  21758  assapropd  21832  psrval  21876  evlslem1  22042  mamucl  22350  mamuass  22351  mamudi  22352  mamudir  22353  mamuvs1  22354  mamuvs2  22355  mamulid  22390  mamurid  22391  dmatsubcl  22447  dmatmulcl  22449  scmatscm  22462  marrepval  22511  marepveval  22517  mdetunilem7  22567  gsummatr01lem4  22607  cpmatmcllem  22667  mat2pmatf1  22678  mat2pmatlin  22684  decpmatmul  22721  pm2mpmhmlem2  22768  chpidmat  22796  pptbas  22957  toponmre  23042  restbas  23107  iscncl  23218  cnrest2  23235  cnpdis  23242  lmcnp  23253  dishaus  23331  cmpcovf  23340  tgcmp  23350  dfconn2  23368  clsconn  23379  2ndcctbss  23404  dis2ndc  23409  1stccnp  23411  islly2  23433  cldllycmp  23444  locfincmp  23475  comppfsc  23481  kgentopon  23487  txcls  23553  ptpjopn  23561  dfac14  23567  xkoccn  23568  txcnp  23569  txcmpb  23593  txlm  23597  xkopt  23604  xkoco1cn  23606  xkoco2cn  23607  qtopcn  23663  qtoprest  23666  regr1lem2  23689  xkocnv  23763  qtophmeo  23766  fmfnfmlem4  23906  hausflim  23930  hauspwpwf1  23936  fclscmp  23979  alexsublem  23993  alexsubALTlem2  23997  alexsubALTlem3  23998  ptcmplem3  24003  ptcmplem4  24004  ptcmplem5  24005  cnextfun  24013  tmdgsum2  24045  symgtgp  24055  tsmsval2  24079  tsmsgsum  24088  utoptop  24183  ismet2  24282  blin  24370  metss2lem  24460  methaus  24469  met1stc  24470  met2ndci  24471  prdsxmslem2  24478  metcnp3  24489  metcnpi3  24495  metustto  24502  metustfbas  24506  nlmvscn  24636  nrginvrcn  24641  xrsxmet  24759  reconnlem1  24776  reconn  24778  xrge0tsms  24784  xmetdcn2  24787  metdscn  24806  addcnlem  24814  fsumcn  24822  cnheiborlem  24914  cnheibor  24915  bndth  24918  lebnum  24924  nmoleub2lem2  25077  ipcn  25207  iscmet3  25254  caubl  25269  rrxdstprj1  25370  minveclem3b  25389  minveclem7  25396  pjthlem2  25399  pmltpc  25412  volfiniun  25509  ioombl1  25524  dyadss  25556  dyaddisjlem  25557  dyadmax  25560  dyadmbllem  25561  opnmbllem  25563  itg1addlem2  25659  itg10a  25672  mbfi1fseqlem6  25682  itg2seq  25704  itg2monolem1  25712  itg2gt0  25722  itgfsum  25789  limcfval  25834  ellimc2  25839  ellimc3  25841  limcres  25848  limciun  25856  dvres  25873  dveflem  25944  rolle  25955  dvlip2  25961  c1liplem1  25962  dvgt0lem1  25968  dvgt0  25970  dvlt0  25971  dvne0  25977  dvfsumrlimge0  25998  ftc1lem6  26009  itgsubst  26017  mdegmullem  26044  ply1domn  26090  ply1divex  26103  fta1g  26136  fta1b  26138  plyf  26164  dgrlem  26195  coeid  26204  plydivalg  26268  aannenlem1  26297  aalioulem3  26303  aalioulem6  26306  abelthlem8  26410  efif1olem4  26515  chordthm  26808  xrlimcnp  26939  jensen  26960  lgamcvglem  27011  lgamcvg2  27026  sqf11  27110  fsumvma2  27186  perfectlem2  27202  lgsdilem  27296  lgsquad2lem2  27357  lgsquad3  27359  2sqlem5  27394  2sqlem9  27399  2sqb  27404  rpvmasumlem  27459  dchrisum0flb  27482  dchrisum0  27492  pntpbnd  27560  pntibndlem3  27564  pntleml  27583  nolt02o  27668  nosupbday  27678  nosupbnd2  27689  noinfbday  27693  noinfbnd2  27704  noetasuplem4  27709  noetainflem4  27713  noetalem1  27714  conway  27780  lesrec  27800  ltslpss  27909  addsprop  27977  bdayons  28277  n0fincut  28356  eucliddivs  28377  remulscllem2  28502  tgjustc1  28552  tgjustc2  28553  legov  28662  legtrid  28668  tglinethru  28713  tglnpt2  28718  tglineintmo  28719  mirreu3  28731  perpcom  28790  colperpexlem3  28809  mideu  28815  opphllem1  28824  hlpasch  28833  lnopp2hpgb  28840  trgcopy  28881  brcgr  28978  brbtwn2  28983  colinearalg  28988  axsegcon  29005  axeuclidlem  29040  axcontlem9  29050  ecgrtg  29061  elntg  29062  eengtrkg  29064  upgr1eopALT  29195  usgredg4  29295  subuhgr  29364  subumgr  29366  usgr2wspthon  30046  clwlkclwwlkf1  30090  eupth2lems  30318  n4cyclfrgr  30371  vacn  30774  blocni  30885  ubthlem3  30952  minvecolem7  30963  chocunii  31381  pjhthmo  31382  pjhthlem2  31472  kbass5  32200  mdsymlem5  32487  foresf1o  32583  fcobij  32802  xrofsup  32850  mgcoval  33071  mgcf1o  33088  xrge0tsmsd  33159  symgcntz  33171  archirngz  33275  archiabllem2a  33280  isarchiofld  33285  prmidl2  33526  mplvrpmmhm  33715  constrelextdg2  33917  smatrcl  33966  reff  34009  ordtconnlem1  34094  qqhval2  34152  volmeas  34401  fiunelcarsg  34486  ballotlemfc0  34663  ballotlemfcc  34664  signstfvneq0  34742  derangenlem  35378  erdsze2lem1  35410  pconnconn  35438  connpconn  35442  cvxsconn  35450  cvmliftmolem2  35489  cvmliftmo  35491  cvmlift2lem10  35519  cvmlift2lem12  35521  cvmlift3lem7  35532  mrsubff1  35721  msubff1  35763  r1peuqusdeg1  35850  ifscgr  36251  cgrxfr  36262  btwnconn1lem13  36306  btwnconn1lem14  36307  outsideofeq  36337  ellines  36359  finminlem  36525  fnejoin2  36576  weiunso  36673  unbdqndv2  36724  irrdiff  37544  poimirlem13  37847  poimirlem14  37848  poimirlem32  37866  opnmbllem0  37870  mblfinlem3  37873  itg2addnclem  37885  itg2addnc  37888  ftc1cnnc  37906  upixp  37943  filbcmb  37954  sstotbnd2  37988  isbnd3  37998  prdsbnd2  38009  cntotbnd  38010  ismtyima  38017  bfp  38038  rrncmslem  38046  unichnidl  38245  lshpcmp  39327  islshpat  39356  lfl0f  39408  ishlat3N  39693  3dim1  39806  islvol5  39918  lvoli2  39920  lncvrelatN  40120  pclfinclN  40289  pexmidlem8N  40316  idltrn  40489  cdleme42keg  40825  cdleme42mgN  40827  cdlemf2  40901  cdlemg2cex  40930  trlcoat  41062  dihopelvalcpre  41587  dih1dimatlem  41668  dihjatcclem4  41760  lcfl7N  41840  lcfrlem9  41889  mapdh9a  42128  hdmapglem7  42268  aks4d1p8  42420  isprimroot  42426  evl1gprodd  42450  sticksstones11  42489  grpods  42527  aks5lem8  42534  renegeulemv  42701  sn-subeu  42760  remulinvcom  42766  imacrhmcl  42847  fidomncyc  42868  fsuppind  42911  fsuppssind  42914  mhpind  42915  prjspertr  42926  prjspreln0  42930  flt4lem7  42980  nna4b4nsq  42981  nacsfix  43032  mzpsubst  43068  mzpcompact2lem  43071  eldioph2lem2  43081  eldioph2  43082  eldioph2b  43083  diophin  43092  diophun  43093  irrapxlem3  43144  irrapxlem5  43146  pell1234qrreccl  43174  pell1234qrmulcl  43175  pell14qrdich  43189  pell1qrge1  43190  pell1qrgaplem  43193  monotuz  43261  acongtr  43298  acongrep  43300  jm2.23  43316  jm2.26a  43320  jm2.26lem3  43321  jm2.26  43322  jm2.27  43328  wepwsolem  43362  fnwe2lem2  43371  kelac1  43383  kercvrlsm  43403  hbtlem5  43448  hbt  43450  mpaaeu  43470  cantnfresb  43644  onmcl  43651  tfsconcatun  43657  tfsconcatfn  43658  tfsconcatfv1  43659  tfsconcatfv2  43660  naddcnff  43682  rfovcnvf1od  44323  mnurndlem1  44600  cncmpmax  45355  rfcnnnub  45359  disjxp1  45392  iccintsng  45846  fprodcn  45923  lptioo2  45954  lptioo1  45955  limclner  45972  stoweidlem31  46352  stoweidlem34  46355  stoweidlem35  46356  stoweidlem49  46370  stoweidlem59  46380  stoweidlem62  46383  fourierdlem60  46487  fourierdlem61  46488  fourierdlem87  46514  iundjiun  46781  ismeannd  46788  hoidmvle  46921  smfsuplem2  47133  2reu8i  47436  prproropf1olem2  47827  paireqne  47834  perfectALTVlem2  48045  mogoldbb  48108  bgoldbtbndlem2  48129  bgoldbtbndlem3  48130  grimedg  48258  grlimprclnbgrvtx  48322  scmsuppss  48694  lindslinindsimp2lem5  48785  elfzolborelfzop1  48842  elbigolo1  48880  itschlc0xyqsol1  49089  itschlc0xyqsol  49090  iccdisj  49220  toslat  49304  iinfssclem3  49378  iinfssc  49379  iinfsubc  49380  imasubc3  49478  upciclem4  49491  uppropd  49503  natoppf  49551  tposcurf1  49621  fuco22  49661  fuco22natlem  49667  functhinclem4  49769  arweuthinc  49851