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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  disjxiun  5050  frpomin  6194  fsnex  7093  f1prex  7094  isotr  7145  weniso  7163  riota5f  7199  fprlem2  8042  tfrlem9a  8122  oaass  8289  oeeui  8330  oaabs2  8374  resixpfo  8617  omxpenlem  8746  pw2f1olem  8749  fopwdom  8753  fofinf1o  8951  marypha1lem  9049  ordiso2  9131  oismo  9156  ixpiunwdom  9206  cantnf  9308  fseqenlem1  9638  iunfictbso  9728  dfac12lem2  9758  dfac12lem3  9759  infunsdom1  9827  infpssrlem5  9921  fin23lem24  9936  isf32lem2  9968  isf32lem4  9970  isf34lem4  9991  fin1a2lem12  10025  fin1a2lem13  10026  ttukeylem6  10128  fpwwe2lem11  10255  fpwwe2lem12  10256  fpwwe2  10257  winalim2  10310  wunex2  10352  tskord  10394  prlem934  10647  mulcmpblnr  10685  dedekind  10995  addid1  11012  cnegex  11013  negeu  11068  add20  11344  divdivdiv  11533  ltmul12a  11688  lemul12a  11690  lediv12a  11725  supaddc  11799  supmul1  11801  cru  11822  uzwo3  12539  xleadd1a  12843  xmullem  12854  xmulgt0  12873  xlemul1a  12878  ixxun  12951  ixxss12  12955  ioodisj  13070  fz0fzelfz0  13218  mulexpz  13675  rpexpmord  13738  leexp1a  13745  expmulnbnd  13802  hashf1  14023  fi1uzind  14063  brfi1indALT  14066  swrdccat  14300  reuccatpfxs1  14312  abs3lem  14902  rexanre  14910  cau3lem  14918  limsupgre  15042  limsupbnd2  15044  o1lo1  15098  rlimclim1  15106  rlimclim  15107  rlimcn1  15149  rlimcn3  15151  o1of2  15174  o1rlimmul  15180  lo1add  15188  lo1mul  15189  isercolllem1  15228  climcau  15234  caucvgrlem  15236  caucvgb  15243  summolem2  15280  summo  15281  modfsummod  15358  o1fsum  15377  prodmolem2  15497  addmodlteqALT  15886  rpdvds  16217  isprm5  16264  isprm6  16271  pclem  16391  pcqmul  16406  pcexp  16412  pcneg  16427  pcprmpw2  16435  pcadd  16442  pcmpt  16445  4sqlem13  16510  vdwlem2  16535  vdwlem7  16540  vdwlem12  16545  ramval  16561  ramub2  16567  ramz2  16577  ramcl  16582  cshwshashlem2  16650  imasval  17016  imasdsval  17020  mreexexd  17151  acsfn  17162  issubc3  17355  idfucl  17387  funcres2c  17408  isnat  17454  fucpropd  17486  xpcval  17684  xpcco  17690  prfval  17706  evlf2  17726  evlfcl  17730  curf12  17735  curf1cl  17736  curf2  17737  curfcl  17740  curf2ndf  17755  hof2val  17764  hofcl  17767  hofpropd  17775  yonedalem4a  17783  yonedainv  17789  drsdirfi  17812  pospo  17851  poslubmo  17917  posglbmo  17918  isipodrs  18043  acsinfd  18062  gsumvalx  18148  gsumpropd2lem  18151  ismndd  18195  mndpropd  18198  mhmeql  18252  mndind  18254  frmdup3lem  18293  mhmmnd  18485  issubg4  18562  ssnmz  18582  conjnmzb  18657  f1otrspeq  18839  psgneu  18898  pgpfi  18994  sylow2blem3  19011  slwhash  19013  fislw  19014  sylow3lem2  19017  lsmdisj2  19072  pj1eu  19086  efgredlem  19137  frgpuplem  19162  gexex  19238  frgpnabl  19260  dprdfadd  19407  dpjidcl  19445  pgpfac1lem3  19464  pgpfaclem3  19470  ablfac2  19476  ablsimpgcygd  19493  ablsimpgfind  19497  ablsimpgprmd  19502  ringpropd  19600  islmhm2  20075  lmhmpropd  20110  lbsextlem4  20198  prmirredlem  20459  psgndiflemA  20563  lsmcss  20654  uvcf1  20754  frlmsslsp  20758  frlmup1  20760  assapropd  20831  psrval  20874  evlslem1  21042  mamucl  21298  mamuass  21299  mamudi  21300  mamudir  21301  mamuvs1  21302  mamuvs2  21303  mamulid  21338  mamurid  21339  dmatsubcl  21395  dmatmulcl  21397  scmatscm  21410  marrepval  21459  marepveval  21465  mdetunilem7  21515  gsummatr01lem4  21555  cpmatmcllem  21615  mat2pmatf1  21626  mat2pmatlin  21632  decpmatmul  21669  pm2mpmhmlem2  21716  chpidmat  21744  pptbas  21905  toponmre  21990  restbas  22055  iscncl  22166  cnrest2  22183  cnpdis  22190  lmcnp  22201  dishaus  22279  cmpcovf  22288  tgcmp  22298  dfconn2  22316  clsconn  22327  2ndcctbss  22352  dis2ndc  22357  1stccnp  22359  islly2  22381  cldllycmp  22392  locfincmp  22423  comppfsc  22429  kgentopon  22435  txcls  22501  ptpjopn  22509  dfac14  22515  xkoccn  22516  txcnp  22517  txcmpb  22541  txlm  22545  xkopt  22552  xkoco1cn  22554  xkoco2cn  22555  qtopcn  22611  qtoprest  22614  regr1lem2  22637  xkocnv  22711  qtophmeo  22714  fmfnfmlem4  22854  hausflim  22878  hauspwpwf1  22884  fclscmp  22927  alexsublem  22941  alexsubALTlem2  22945  alexsubALTlem3  22946  ptcmplem3  22951  ptcmplem4  22952  ptcmplem5  22953  cnextfun  22961  tmdgsum2  22993  symgtgp  23003  tsmsval2  23027  tsmsgsum  23036  utoptop  23132  ismet2  23231  blin  23319  metss2lem  23409  methaus  23418  met1stc  23419  met2ndci  23420  prdsxmslem2  23427  metcnp3  23438  metcnpi3  23444  metustto  23451  metustfbas  23455  nlmvscn  23585  nrginvrcn  23590  xrsxmet  23706  reconnlem1  23723  reconn  23725  xrge0tsms  23731  xmetdcn2  23734  metdscn  23753  addcnlem  23761  fsumcn  23767  cnheiborlem  23851  cnheibor  23852  bndth  23855  lebnum  23861  nmoleub2lem2  24013  ipcn  24143  iscmet3  24190  caubl  24205  rrxdstprj1  24306  minveclem3b  24325  minveclem7  24332  pjthlem2  24335  pmltpc  24347  volfiniun  24444  ioombl1  24459  dyadss  24491  dyaddisjlem  24492  dyadmax  24495  dyadmbllem  24496  opnmbllem  24498  itg1addlem2  24594  itg10a  24608  mbfi1fseqlem6  24618  itg2seq  24640  itg2monolem1  24648  itg2gt0  24658  itgfsum  24724  limcfval  24769  ellimc2  24774  ellimc3  24776  limcres  24783  limciun  24791  dvres  24808  dveflem  24876  rolle  24887  dvlip2  24892  c1liplem1  24893  dvgt0lem1  24899  dvgt0  24901  dvlt0  24902  dvne0  24908  dvfsumrlimge0  24927  ftc1lem6  24938  itgsubst  24946  mdegmullem  24976  ply1domn  25021  ply1divex  25034  fta1g  25065  fta1b  25067  plyf  25092  dgrlem  25123  coeid  25132  plydivalg  25192  aannenlem1  25221  aalioulem3  25227  aalioulem6  25230  abelthlem8  25331  efif1olem4  25434  chordthm  25720  xrlimcnp  25851  jensen  25871  lgamcvglem  25922  lgamcvg2  25937  sqf11  26021  fsumvma2  26095  perfectlem2  26111  lgsdilem  26205  lgsquad2lem2  26266  lgsquad3  26268  2sqlem5  26303  2sqlem9  26308  2sqb  26313  rpvmasumlem  26368  dchrisum0flb  26391  dchrisum0  26401  pntpbnd  26469  pntibndlem3  26473  pntleml  26492  tgjustc1  26566  tgjustc2  26567  legov  26676  legtrid  26682  tglinethru  26727  tglnpt2  26732  tglineintmo  26733  mirreu3  26745  perpcom  26804  colperpexlem3  26823  mideu  26829  opphllem1  26838  hlpasch  26847  lnopp2hpgb  26854  trgcopy  26895  brcgr  26991  brbtwn2  26996  colinearalg  27001  axsegcon  27018  axeuclidlem  27053  axcontlem9  27063  ecgrtg  27074  elntg  27075  eengtrkg  27077  upgr1eopALT  27208  usgredg4  27305  subuhgr  27374  subumgr  27376  usgr2wspthon  28049  clwlkclwwlkf1  28093  eupth2lems  28321  n4cyclfrgr  28374  vacn  28775  blocni  28886  ubthlem3  28953  minvecolem7  28964  chocunii  29382  pjhthmo  29383  pjhthlem2  29473  kbass5  30201  mdsymlem5  30488  foresf1o  30569  fcobij  30777  xrofsup  30810  mgcoval  30983  mgcf1o  31000  xrge0tsmsd  31036  symgcntz  31073  archirngz  31162  archiabllem2a  31167  isarchiofld  31235  prmidl2  31330  smatrcl  31460  reff  31503  ordtconnlem1  31588  qqhval2  31644  volmeas  31911  fiunelcarsg  31995  ballotlemfc0  32171  ballotlemfcc  32172  signstfvneq0  32263  derangenlem  32846  erdsze2lem1  32878  pconnconn  32906  connpconn  32910  cvxsconn  32918  cvmliftmolem2  32957  cvmliftmo  32959  cvmlift2lem10  32987  cvmlift2lem12  32989  cvmlift3lem7  33000  mrsubff1  33189  msubff1  33231  ttrclss  33519  frxp2  33528  frxp3  33534  poseq  33539  naddssim  33574  nolt02o  33635  nosupbday  33645  nosupbnd2  33656  noinfbday  33660  noinfbnd2  33671  noetasuplem4  33676  noetainflem4  33680  noetalem1  33681  conway  33730  slerec  33750  sltlpss  33824  ifscgr  34083  cgrxfr  34094  btwnconn1lem13  34138  btwnconn1lem14  34139  outsideofeq  34169  ellines  34191  finminlem  34244  fnejoin2  34295  unbdqndv2  34428  irrdiff  35231  poimirlem13  35527  poimirlem14  35528  poimirlem32  35546  opnmbllem0  35550  mblfinlem3  35553  itg2addnclem  35565  itg2addnc  35568  ftc1cnnc  35586  upixp  35624  filbcmb  35635  sstotbnd2  35669  isbnd3  35679  prdsbnd2  35690  cntotbnd  35691  ismtyima  35698  bfp  35719  rrncmslem  35727  unichnidl  35926  lshpcmp  36739  islshpat  36768  lfl0f  36820  ishlat3N  37105  3dim1  37218  islvol5  37330  lvoli2  37332  lncvrelatN  37532  pclfinclN  37701  pexmidlem8N  37728  idltrn  37901  cdleme42keg  38237  cdleme42mgN  38239  cdlemf2  38313  cdlemg2cex  38342  trlcoat  38474  dihopelvalcpre  38999  dih1dimatlem  39080  dihjatcclem4  39172  lcfl7N  39252  lcfrlem9  39301  mapdh9a  39540  hdmapglem7  39680  sticksstones11  39834  fsuppind  39989  fsuppssind  39992  mhpind  39993  mhphf  39995  renegeulemv  40059  sn-subeu  40116  remulinvcom  40122  itrere  40144  retire  40145  prjspertr  40152  prjspreln0  40156  flt4lem7  40199  nna4b4nsq  40200  nacsfix  40237  mzpsubst  40273  mzpcompact2lem  40276  eldioph2lem2  40286  eldioph2  40287  eldioph2b  40288  diophin  40297  diophun  40298  irrapxlem3  40349  irrapxlem5  40351  pell1234qrreccl  40379  pell1234qrmulcl  40380  pell14qrdich  40394  pell1qrge1  40395  pell1qrgaplem  40398  monotuz  40466  acongtr  40503  acongrep  40505  jm2.23  40521  jm2.26a  40525  jm2.26lem3  40526  jm2.26  40527  jm2.27  40533  wepwsolem  40570  fnwe2lem2  40579  kelac1  40591  kercvrlsm  40611  hbtlem5  40656  hbt  40658  mpaaeu  40678  rfovcnvf1od  41289  mnurndlem1  41572  cncmpmax  42248  rfcnnnub  42252  disjxp1  42290  iccintsng  42736  fprodcn  42816  lptioo2  42847  lptioo1  42848  limclner  42867  stoweidlem31  43247  stoweidlem34  43250  stoweidlem35  43251  stoweidlem49  43265  stoweidlem59  43275  stoweidlem62  43278  fourierdlem60  43382  fourierdlem61  43383  fourierdlem87  43409  iundjiun  43673  ismeannd  43680  hoidmvle  43813  smfsuplem2  44017  2reu8i  44277  prproropf1olem2  44629  paireqne  44636  perfectALTVlem2  44847  mogoldbb  44910  bgoldbtbndlem2  44931  bgoldbtbndlem3  44932  isomgrtrlem  44963  mgmhmeql  45030  mndpsuppss  45380  scmsuppss  45381  lindslinindsimp2lem5  45476  elfzolborelfzop1  45533  elbigolo1  45576  itschlc0xyqsol1  45785  itschlc0xyqsol  45786  iccdisj  45865  toslat  45941  functhinclem4  45998