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  5104  frpomin  6313  fsnex  7258  f1prex  7259  isotr  7311  weniso  7329  riota5f  7372  frxp2  8123  frxp3  8130  xpord3pred  8131  poseq  8137  fprlem2  8280  tfrlem9a  8354  oaass  8525  oeeui  8566  oaabs2  8613  coflton  8635  cofon1  8636  naddssim  8649  resixpfo  8909  omxpenlem  9042  pw2f1olem  9045  fopwdom  9049  fofinf1o  9283  marypha1lem  9384  ordiso2  9468  oismo  9493  ixpiunwdom  9543  cantnf  9646  ttrclss  9673  fseqenlem1  9977  iunfictbso  10067  dfac12lem2  10098  dfac12lem3  10099  infunsdom1  10165  infpssrlem5  10260  fin23lem24  10275  isf32lem2  10307  isf32lem4  10309  isf34lem4  10330  fin1a2lem12  10364  fin1a2lem13  10365  ttukeylem6  10467  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  winalim2  10649  wunex2  10691  tskord  10733  prlem934  10986  mulcmpblnr  11024  dedekind  11337  addrid  11354  cnegex  11355  negeu  11411  add20  11690  divdivdiv  11883  ltmul12a  12038  lemul12a  12040  lediv12a  12076  supaddc  12150  supmul1  12152  cru  12178  uzwo3  12902  xleadd1a  13213  xmullem  13224  xmulgt0  13243  xlemul1a  13248  ixxun  13322  ixxss12  13326  ioodisj  13443  fz0fzelfz0  13595  mulexpz  14067  rpexpmord  14133  leexp1a  14140  expmulnbnd  14200  hashf1  14422  fi1uzind  14472  brfi1indALT  14475  swrdccat  14700  reuccatpfxs1  14712  abs3lem  15305  rexanre  15313  cau3lem  15321  limsupgre  15447  limsupbnd2  15449  o1lo1  15503  rlimclim1  15511  rlimclim  15512  rlimcn1  15554  rlimcn3  15556  o1of2  15579  o1rlimmul  15585  lo1add  15593  lo1mul  15594  isercolllem1  15631  climcau  15637  caucvgrlem  15639  caucvgb  15646  summolem2  15682  summo  15683  modfsummod  15760  o1fsum  15779  prodmolem2  15901  addmodlteqALT  16295  rpdvds  16630  isprm5  16677  isprm6  16684  pclem  16809  pcqmul  16824  pcexp  16830  pcneg  16845  pcprmpw2  16853  pcadd  16860  pcmpt  16863  4sqlem13  16928  vdwlem2  16953  vdwlem7  16958  vdwlem12  16963  ramval  16979  ramub2  16985  ramz2  16995  ramcl  17000  cshwshashlem2  17067  imasval  17474  imasdsval  17478  mreexexd  17609  acsfn  17620  issubc3  17811  idfucl  17843  funcres2c  17865  isnat  17912  fucpropd  17942  xpcval  18138  xpcco  18144  prfval  18160  evlf2  18179  evlfcl  18183  curf12  18188  curf1cl  18189  curf2  18190  curfcl  18193  curf2ndf  18208  hof2val  18217  hofcl  18220  hofpropd  18228  yonedalem4a  18236  yonedainv  18242  drsdirfi  18266  pospo  18304  poslubmo  18370  posglbmo  18371  isipodrs  18496  acsinfd  18515  gsumvalx  18603  gsumpropd2lem  18606  mgmhmeql  18643  sgrppropd  18658  ismndd  18683  mndpropd  18686  mndpsuppss  18692  mhmeql  18753  mndind  18755  frmdup3lem  18793  mhmmnd  18996  issubg4  19077  ssnmz  19098  conjnmzb  19185  f1otrspeq  19377  psgneu  19436  pgpfi  19535  sylow2blem3  19552  slwhash  19554  fislw  19555  sylow3lem2  19558  lsmdisj2  19612  pj1eu  19626  efgredlem  19677  frgpuplem  19702  gexex  19783  frgpnabl  19805  dprdfadd  19952  dpjidcl  19990  pgpfac1lem3  20009  pgpfaclem3  20015  ablfac2  20021  ablsimpgcygd  20038  ablsimpgfind  20042  ablsimpgprmd  20047  rngpropd  20083  ringpropd  20197  imadrhmcl  20706  islmhm2  20945  lmhmpropd  20980  lbsextlem4  21071  prmirredlem  21382  psgndiflemA  21510  lsmcss  21601  uvcf1  21701  frlmsslsp  21705  frlmup1  21707  assapropd  21781  psrval  21824  evlslem1  21989  mamucl  22288  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  mamulid  22328  mamurid  22329  dmatsubcl  22385  dmatmulcl  22387  scmatscm  22400  marrepval  22449  marepveval  22455  mdetunilem7  22505  gsummatr01lem4  22545  cpmatmcllem  22605  mat2pmatf1  22616  mat2pmatlin  22622  decpmatmul  22659  pm2mpmhmlem2  22706  chpidmat  22734  pptbas  22895  toponmre  22980  restbas  23045  iscncl  23156  cnrest2  23173  cnpdis  23180  lmcnp  23191  dishaus  23269  cmpcovf  23278  tgcmp  23288  dfconn2  23306  clsconn  23317  2ndcctbss  23342  dis2ndc  23347  1stccnp  23349  islly2  23371  cldllycmp  23382  locfincmp  23413  comppfsc  23419  kgentopon  23425  txcls  23491  ptpjopn  23499  dfac14  23505  xkoccn  23506  txcnp  23507  txcmpb  23531  txlm  23535  xkopt  23542  xkoco1cn  23544  xkoco2cn  23545  qtopcn  23601  qtoprest  23604  regr1lem2  23627  xkocnv  23701  qtophmeo  23704  fmfnfmlem4  23844  hausflim  23868  hauspwpwf1  23874  fclscmp  23917  alexsublem  23931  alexsubALTlem2  23935  alexsubALTlem3  23936  ptcmplem3  23941  ptcmplem4  23942  ptcmplem5  23943  cnextfun  23951  tmdgsum2  23983  symgtgp  23993  tsmsval2  24017  tsmsgsum  24026  utoptop  24122  ismet2  24221  blin  24309  metss2lem  24399  methaus  24408  met1stc  24409  met2ndci  24410  prdsxmslem2  24417  metcnp3  24428  metcnpi3  24434  metustto  24441  metustfbas  24445  nlmvscn  24575  nrginvrcn  24580  xrsxmet  24698  reconnlem1  24715  reconn  24717  xrge0tsms  24723  xmetdcn2  24726  metdscn  24745  addcnlem  24753  fsumcn  24761  cnheiborlem  24853  cnheibor  24854  bndth  24857  lebnum  24863  nmoleub2lem2  25016  ipcn  25146  iscmet3  25193  caubl  25208  rrxdstprj1  25309  minveclem3b  25328  minveclem7  25335  pjthlem2  25338  pmltpc  25351  volfiniun  25448  ioombl1  25463  dyadss  25495  dyaddisjlem  25496  dyadmax  25499  dyadmbllem  25500  opnmbllem  25502  itg1addlem2  25598  itg10a  25611  mbfi1fseqlem6  25621  itg2seq  25643  itg2monolem1  25651  itg2gt0  25661  itgfsum  25728  limcfval  25773  ellimc2  25778  ellimc3  25780  limcres  25787  limciun  25795  dvres  25812  dveflem  25883  rolle  25894  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  dvgt0  25909  dvlt0  25910  dvne0  25916  dvfsumrlimge0  25937  ftc1lem6  25948  itgsubst  25956  mdegmullem  25983  ply1domn  26029  ply1divex  26042  fta1g  26075  fta1b  26077  plyf  26103  dgrlem  26134  coeid  26143  plydivalg  26207  aannenlem1  26236  aalioulem3  26242  aalioulem6  26245  abelthlem8  26349  efif1olem4  26454  chordthm  26747  xrlimcnp  26878  jensen  26899  lgamcvglem  26950  lgamcvg2  26965  sqf11  27049  fsumvma2  27125  perfectlem2  27141  lgsdilem  27235  lgsquad2lem2  27296  lgsquad3  27298  2sqlem5  27333  2sqlem9  27338  2sqb  27343  rpvmasumlem  27398  dchrisum0flb  27421  dchrisum0  27431  pntpbnd  27499  pntibndlem3  27503  pntleml  27522  nolt02o  27607  nosupbday  27617  nosupbnd2  27628  noinfbday  27632  noinfbnd2  27643  noetasuplem4  27648  noetainflem4  27652  noetalem1  27653  conway  27711  slerec  27731  sltlpss  27819  addsprop  27883  bdayon  28173  n0sfincut  28246  eucliddivs  28265  remulscllem2  28352  tgjustc1  28402  tgjustc2  28403  legov  28512  legtrid  28518  tglinethru  28563  tglnpt2  28568  tglineintmo  28569  mirreu3  28581  perpcom  28640  colperpexlem3  28659  mideu  28665  opphllem1  28674  hlpasch  28683  lnopp2hpgb  28690  trgcopy  28731  brcgr  28827  brbtwn2  28832  colinearalg  28837  axsegcon  28854  axeuclidlem  28889  axcontlem9  28899  ecgrtg  28910  elntg  28911  eengtrkg  28913  upgr1eopALT  29044  usgredg4  29144  subuhgr  29213  subumgr  29215  usgr2wspthon  29895  clwlkclwwlkf1  29939  eupth2lems  30167  n4cyclfrgr  30220  vacn  30623  blocni  30734  ubthlem3  30801  minvecolem7  30812  chocunii  31230  pjhthmo  31231  pjhthlem2  31321  kbass5  32049  mdsymlem5  32336  foresf1o  32433  fcobij  32645  xrofsup  32690  mgcoval  32912  mgcf1o  32929  xrge0tsmsd  33002  symgcntz  33042  archirngz  33143  archiabllem2a  33148  isarchiofld  33295  prmidl2  33412  constrelextdg2  33737  smatrcl  33786  reff  33829  ordtconnlem1  33914  qqhval2  33972  volmeas  34221  fiunelcarsg  34307  ballotlemfc0  34484  ballotlemfcc  34485  signstfvneq0  34563  derangenlem  35158  erdsze2lem1  35190  pconnconn  35218  connpconn  35222  cvxsconn  35230  cvmliftmolem2  35269  cvmliftmo  35271  cvmlift2lem10  35299  cvmlift2lem12  35301  cvmlift3lem7  35312  mrsubff1  35501  msubff1  35543  r1peuqusdeg1  35630  ifscgr  36032  cgrxfr  36043  btwnconn1lem13  36087  btwnconn1lem14  36088  outsideofeq  36118  ellines  36140  finminlem  36306  fnejoin2  36357  weiunso  36454  unbdqndv2  36499  irrdiff  37314  poimirlem13  37627  poimirlem14  37628  poimirlem32  37646  opnmbllem0  37650  mblfinlem3  37653  itg2addnclem  37665  itg2addnc  37668  ftc1cnnc  37686  upixp  37723  filbcmb  37734  sstotbnd2  37768  isbnd3  37778  prdsbnd2  37789  cntotbnd  37790  ismtyima  37797  bfp  37818  rrncmslem  37826  unichnidl  38025  lshpcmp  38981  islshpat  39010  lfl0f  39062  ishlat3N  39347  3dim1  39461  islvol5  39573  lvoli2  39575  lncvrelatN  39775  pclfinclN  39944  pexmidlem8N  39971  idltrn  40144  cdleme42keg  40480  cdleme42mgN  40482  cdlemf2  40556  cdlemg2cex  40585  trlcoat  40717  dihopelvalcpre  41242  dih1dimatlem  41323  dihjatcclem4  41415  lcfl7N  41495  lcfrlem9  41544  mapdh9a  41783  hdmapglem7  41923  aks4d1p8  42075  isprimroot  42081  evl1gprodd  42105  sticksstones11  42144  grpods  42182  aks5lem8  42189  renegeulemv  42356  sn-subeu  42415  remulinvcom  42421  imacrhmcl  42502  fidomncyc  42523  fsuppind  42578  fsuppssind  42581  mhpind  42582  prjspertr  42593  prjspreln0  42597  flt4lem7  42647  nna4b4nsq  42648  nacsfix  42700  mzpsubst  42736  mzpcompact2lem  42739  eldioph2lem2  42749  eldioph2  42750  eldioph2b  42751  diophin  42760  diophun  42761  irrapxlem3  42812  irrapxlem5  42814  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrdich  42857  pell1qrge1  42858  pell1qrgaplem  42861  monotuz  42930  acongtr  42967  acongrep  42969  jm2.23  42985  jm2.26a  42989  jm2.26lem3  42990  jm2.26  42991  jm2.27  42997  wepwsolem  43031  fnwe2lem2  43040  kelac1  43052  kercvrlsm  43072  hbtlem5  43117  hbt  43119  mpaaeu  43139  cantnfresb  43313  onmcl  43320  tfsconcatun  43326  tfsconcatfn  43327  tfsconcatfv1  43328  tfsconcatfv2  43329  naddcnff  43351  rfovcnvf1od  43993  mnurndlem1  44270  cncmpmax  45026  rfcnnnub  45030  disjxp1  45063  iccintsng  45521  fprodcn  45598  lptioo2  45629  lptioo1  45630  limclner  45649  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem49  46047  stoweidlem59  46057  stoweidlem62  46060  fourierdlem60  46164  fourierdlem61  46165  fourierdlem87  46191  iundjiun  46458  ismeannd  46465  hoidmvle  46598  smfsuplem2  46810  2reu8i  47114  prproropf1olem2  47505  paireqne  47512  perfectALTVlem2  47723  mogoldbb  47786  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  grimedg  47935  scmsuppss  48359  lindslinindsimp2lem5  48451  elfzolborelfzop1  48508  elbigolo1  48546  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  iccdisj  48886  toslat  48970  iinfssclem3  49045  iinfssc  49046  iinfsubc  49047  imasubc3  49145  upciclem4  49158  uppropd  49170  natoppf  49218  tposcurf1  49288  fuco22  49328  fuco22natlem  49334  functhinclem4  49436  arweuthinc  49518