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 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  5144  frpomin  6362  fsnex  7302  f1prex  7303  isotr  7355  weniso  7373  riota5f  7415  frxp2  8167  frxp3  8174  xpord3pred  8175  poseq  8181  fprlem2  8324  tfrlem9a  8424  oaass  8597  oeeui  8638  oaabs2  8685  coflton  8707  cofon1  8708  naddssim  8721  resixpfo  8974  omxpenlem  9111  pw2f1olem  9114  fopwdom  9118  fofinf1o  9369  marypha1lem  9470  ordiso2  9552  oismo  9577  ixpiunwdom  9627  cantnf  9730  ttrclss  9757  fseqenlem1  10061  iunfictbso  10151  dfac12lem2  10182  dfac12lem3  10183  infunsdom1  10249  infpssrlem5  10344  fin23lem24  10359  isf32lem2  10391  isf32lem4  10393  isf34lem4  10414  fin1a2lem12  10448  fin1a2lem13  10449  ttukeylem6  10551  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  winalim2  10733  wunex2  10775  tskord  10817  prlem934  11070  mulcmpblnr  11108  dedekind  11421  addrid  11438  cnegex  11439  negeu  11495  add20  11772  divdivdiv  11965  ltmul12a  12120  lemul12a  12122  lediv12a  12158  supaddc  12232  supmul1  12234  cru  12255  uzwo3  12982  xleadd1a  13291  xmullem  13302  xmulgt0  13321  xlemul1a  13326  ixxun  13399  ixxss12  13403  ioodisj  13518  fz0fzelfz0  13670  mulexpz  14139  rpexpmord  14204  leexp1a  14211  expmulnbnd  14270  hashf1  14492  fi1uzind  14542  brfi1indALT  14545  swrdccat  14769  reuccatpfxs1  14781  abs3lem  15373  rexanre  15381  cau3lem  15389  limsupgre  15513  limsupbnd2  15515  o1lo1  15569  rlimclim1  15577  rlimclim  15578  rlimcn1  15620  rlimcn3  15622  o1of2  15645  o1rlimmul  15651  lo1add  15659  lo1mul  15660  isercolllem1  15697  climcau  15703  caucvgrlem  15705  caucvgb  15712  summolem2  15748  summo  15749  modfsummod  15826  o1fsum  15845  prodmolem2  15967  addmodlteqALT  16358  rpdvds  16693  isprm5  16740  isprm6  16747  pclem  16871  pcqmul  16886  pcexp  16892  pcneg  16907  pcprmpw2  16915  pcadd  16922  pcmpt  16925  4sqlem13  16990  vdwlem2  17015  vdwlem7  17020  vdwlem12  17025  ramval  17041  ramub2  17047  ramz2  17057  ramcl  17062  cshwshashlem2  17130  imasval  17557  imasdsval  17561  mreexexd  17692  acsfn  17703  issubc3  17899  idfucl  17931  funcres2c  17954  isnat  18001  fucpropd  18033  xpcval  18232  xpcco  18238  prfval  18254  evlf2  18274  evlfcl  18278  curf12  18283  curf1cl  18284  curf2  18285  curfcl  18288  curf2ndf  18303  hof2val  18312  hofcl  18315  hofpropd  18323  yonedalem4a  18331  yonedainv  18337  drsdirfi  18362  pospo  18402  poslubmo  18468  posglbmo  18469  isipodrs  18594  acsinfd  18613  gsumvalx  18701  gsumpropd2lem  18704  mgmhmeql  18741  sgrppropd  18756  ismndd  18781  mndpropd  18784  mndpsuppss  18790  mhmeql  18851  mndind  18853  frmdup3lem  18891  mhmmnd  19094  issubg4  19175  ssnmz  19196  conjnmzb  19283  f1otrspeq  19479  psgneu  19538  pgpfi  19637  sylow2blem3  19654  slwhash  19656  fislw  19657  sylow3lem2  19660  lsmdisj2  19714  pj1eu  19728  efgredlem  19779  frgpuplem  19804  gexex  19885  frgpnabl  19907  dprdfadd  20054  dpjidcl  20092  pgpfac1lem3  20111  pgpfaclem3  20117  ablfac2  20123  ablsimpgcygd  20140  ablsimpgfind  20144  ablsimpgprmd  20149  rngpropd  20191  ringpropd  20301  imadrhmcl  20814  islmhm2  21054  lmhmpropd  21089  lbsextlem4  21180  prmirredlem  21500  psgndiflemA  21636  lsmcss  21727  uvcf1  21829  frlmsslsp  21833  frlmup1  21835  assapropd  21909  psrval  21952  evlslem1  22123  mamucl  22420  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  mamulid  22462  mamurid  22463  dmatsubcl  22519  dmatmulcl  22521  scmatscm  22534  marrepval  22583  marepveval  22589  mdetunilem7  22639  gsummatr01lem4  22679  cpmatmcllem  22739  mat2pmatf1  22750  mat2pmatlin  22756  decpmatmul  22793  pm2mpmhmlem2  22840  chpidmat  22868  pptbas  23030  toponmre  23116  restbas  23181  iscncl  23292  cnrest2  23309  cnpdis  23316  lmcnp  23327  dishaus  23405  cmpcovf  23414  tgcmp  23424  dfconn2  23442  clsconn  23453  2ndcctbss  23478  dis2ndc  23483  1stccnp  23485  islly2  23507  cldllycmp  23518  locfincmp  23549  comppfsc  23555  kgentopon  23561  txcls  23627  ptpjopn  23635  dfac14  23641  xkoccn  23642  txcnp  23643  txcmpb  23667  txlm  23671  xkopt  23678  xkoco1cn  23680  xkoco2cn  23681  qtopcn  23737  qtoprest  23740  regr1lem2  23763  xkocnv  23837  qtophmeo  23840  fmfnfmlem4  23980  hausflim  24004  hauspwpwf1  24010  fclscmp  24053  alexsublem  24067  alexsubALTlem2  24071  alexsubALTlem3  24072  ptcmplem3  24077  ptcmplem4  24078  ptcmplem5  24079  cnextfun  24087  tmdgsum2  24119  symgtgp  24129  tsmsval2  24153  tsmsgsum  24162  utoptop  24258  ismet2  24358  blin  24446  metss2lem  24539  methaus  24548  met1stc  24549  met2ndci  24550  prdsxmslem2  24557  metcnp3  24568  metcnpi3  24574  metustto  24581  metustfbas  24585  nlmvscn  24723  nrginvrcn  24728  xrsxmet  24844  reconnlem1  24861  reconn  24863  xrge0tsms  24869  xmetdcn2  24872  metdscn  24891  addcnlem  24899  fsumcn  24907  cnheiborlem  24999  cnheibor  25000  bndth  25003  lebnum  25009  nmoleub2lem2  25162  ipcn  25293  iscmet3  25340  caubl  25355  rrxdstprj1  25456  minveclem3b  25475  minveclem7  25482  pjthlem2  25485  pmltpc  25498  volfiniun  25595  ioombl1  25610  dyadss  25642  dyaddisjlem  25643  dyadmax  25646  dyadmbllem  25647  opnmbllem  25649  itg1addlem2  25745  itg10a  25759  mbfi1fseqlem6  25769  itg2seq  25791  itg2monolem1  25799  itg2gt0  25809  itgfsum  25876  limcfval  25921  ellimc2  25926  ellimc3  25928  limcres  25935  limciun  25943  dvres  25960  dveflem  26031  rolle  26042  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  dvgt0  26057  dvlt0  26058  dvne0  26064  dvfsumrlimge0  26085  ftc1lem6  26096  itgsubst  26104  mdegmullem  26131  ply1domn  26177  ply1divex  26190  fta1g  26223  fta1b  26225  plyf  26251  dgrlem  26282  coeid  26291  plydivalg  26355  aannenlem1  26384  aalioulem3  26390  aalioulem6  26393  abelthlem8  26497  efif1olem4  26601  chordthm  26894  xrlimcnp  27025  jensen  27046  lgamcvglem  27097  lgamcvg2  27112  sqf11  27196  fsumvma2  27272  perfectlem2  27288  lgsdilem  27382  lgsquad2lem2  27443  lgsquad3  27445  2sqlem5  27480  2sqlem9  27485  2sqb  27490  rpvmasumlem  27545  dchrisum0flb  27568  dchrisum0  27578  pntpbnd  27646  pntibndlem3  27650  pntleml  27669  nolt02o  27754  nosupbday  27764  nosupbnd2  27775  noinfbday  27779  noinfbnd2  27790  noetasuplem4  27795  noetainflem4  27799  noetalem1  27800  conway  27858  slerec  27878  sltlpss  27959  addsprop  28023  remulscllem2  28447  tgjustc1  28497  tgjustc2  28498  legov  28607  legtrid  28613  tglinethru  28658  tglnpt2  28663  tglineintmo  28664  mirreu3  28676  perpcom  28735  colperpexlem3  28754  mideu  28760  opphllem1  28769  hlpasch  28778  lnopp2hpgb  28785  trgcopy  28826  brcgr  28929  brbtwn2  28934  colinearalg  28939  axsegcon  28956  axeuclidlem  28991  axcontlem9  29001  ecgrtg  29012  elntg  29013  eengtrkg  29015  upgr1eopALT  29148  usgredg4  29248  subuhgr  29317  subumgr  29319  usgr2wspthon  29994  clwlkclwwlkf1  30038  eupth2lems  30266  n4cyclfrgr  30319  vacn  30722  blocni  30833  ubthlem3  30900  minvecolem7  30911  chocunii  31329  pjhthmo  31330  pjhthlem2  31420  kbass5  32148  mdsymlem5  32435  foresf1o  32531  fcobij  32739  xrofsup  32777  mgcoval  32960  mgcf1o  32977  xrge0tsmsd  33047  symgcntz  33087  archirngz  33178  archiabllem2a  33183  isarchiofld  33326  prmidl2  33448  constrelextdg2  33751  smatrcl  33756  reff  33799  ordtconnlem1  33884  qqhval2  33944  volmeas  34211  fiunelcarsg  34297  ballotlemfc0  34473  ballotlemfcc  34474  signstfvneq0  34565  derangenlem  35155  erdsze2lem1  35187  pconnconn  35215  connpconn  35219  cvxsconn  35227  cvmliftmolem2  35266  cvmliftmo  35268  cvmlift2lem10  35296  cvmlift2lem12  35298  cvmlift3lem7  35309  mrsubff1  35498  msubff1  35540  r1peuqusdeg1  35627  ifscgr  36025  cgrxfr  36036  btwnconn1lem13  36080  btwnconn1lem14  36081  outsideofeq  36111  ellines  36133  finminlem  36300  fnejoin2  36351  weiunso  36448  unbdqndv2  36493  irrdiff  37308  poimirlem13  37619  poimirlem14  37620  poimirlem32  37638  opnmbllem0  37642  mblfinlem3  37645  itg2addnclem  37657  itg2addnc  37660  ftc1cnnc  37678  upixp  37715  filbcmb  37726  sstotbnd2  37760  isbnd3  37770  prdsbnd2  37781  cntotbnd  37782  ismtyima  37789  bfp  37810  rrncmslem  37818  unichnidl  38017  lshpcmp  38969  islshpat  38998  lfl0f  39050  ishlat3N  39335  3dim1  39449  islvol5  39561  lvoli2  39563  lncvrelatN  39763  pclfinclN  39932  pexmidlem8N  39959  idltrn  40132  cdleme42keg  40468  cdleme42mgN  40470  cdlemf2  40544  cdlemg2cex  40573  trlcoat  40705  dihopelvalcpre  41230  dih1dimatlem  41311  dihjatcclem4  41403  lcfl7N  41483  lcfrlem9  41532  mapdh9a  41771  hdmapglem7  41911  aks4d1p8  42068  isprimroot  42074  evl1gprodd  42098  sticksstones11  42137  grpods  42175  aks5lem8  42182  renegeulemv  42374  sn-subeu  42432  remulinvcom  42438  sn-itrere  42474  sn-retire  42475  imacrhmcl  42500  fidomncyc  42521  fsuppind  42576  fsuppssind  42579  mhpind  42580  prjspertr  42591  prjspreln0  42595  flt4lem7  42645  nna4b4nsq  42646  nacsfix  42699  mzpsubst  42735  mzpcompact2lem  42738  eldioph2lem2  42748  eldioph2  42749  eldioph2b  42750  diophin  42759  diophun  42760  irrapxlem3  42811  irrapxlem5  42813  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrdich  42856  pell1qrge1  42857  pell1qrgaplem  42860  monotuz  42929  acongtr  42966  acongrep  42968  jm2.23  42984  jm2.26a  42988  jm2.26lem3  42989  jm2.26  42990  jm2.27  42996  wepwsolem  43030  fnwe2lem2  43039  kelac1  43051  kercvrlsm  43071  hbtlem5  43116  hbt  43118  mpaaeu  43138  cantnfresb  43313  onmcl  43320  tfsconcatun  43326  tfsconcatfn  43327  tfsconcatfv1  43328  tfsconcatfv2  43329  naddcnff  43351  rfovcnvf1od  43993  mnurndlem1  44276  cncmpmax  44969  rfcnnnub  44973  disjxp1  45008  iccintsng  45475  fprodcn  45555  lptioo2  45586  lptioo1  45587  limclner  45606  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem49  46004  stoweidlem59  46014  stoweidlem62  46017  fourierdlem60  46121  fourierdlem61  46122  fourierdlem87  46148  iundjiun  46415  ismeannd  46422  hoidmvle  46555  smfsuplem2  46767  2reu8i  47062  prproropf1olem2  47428  paireqne  47435  perfectALTVlem2  47646  mogoldbb  47709  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  uspgrimprop  47810  grimedg  47840  scmsuppss  48215  lindslinindsimp2lem5  48307  elfzolborelfzop1  48364  elbigolo1  48406  itschlc0xyqsol1  48615  itschlc0xyqsol  48616  iccdisj  48694  toslat  48770  upciclem4  48814  functhinclem4  48843