Theorem simplrr 776

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5065  fsnex  7041  f1prex  7042  isotr  7091  weniso  7109  riota5f  7144  tfrlem9a  8024  oaass  8189  oeeui  8230  oaabs2  8274  resixpfo  8502  omxpenlem  8620  pw2f1olem  8623  fopwdom  8627  fofinf1o  8801  marypha1lem  8899  ordiso2  8981  oismo  9006  ixpiunwdom  9057  cantnf  9158  fseqenlem1  9452  iunfictbso  9542  dfac12lem2  9572  dfac12lem3  9573  infunsdom1  9637  infpssrlem5  9731  fin23lem24  9746  isf32lem2  9778  isf32lem4  9780  isf34lem4  9801  fin1a2lem12  9835  fin1a2lem13  9836  ttukeylem6  9938  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  winalim2  10120  wunex2  10162  tskord  10204  prlem934  10457  mulcmpblnr  10495  dedekind  10805  addid1  10822  cnegex  10823  negeu  10878  add20  11154  divdivdiv  11343  ltmul12a  11498  lemul12a  11500  lediv12a  11535  supaddc  11610  supmul1  11612  cru  11632  uzwo3  12346  xleadd1a  12649  xmullem  12660  xmulgt0  12679  xlemul1a  12684  ixxun  12757  ixxss12  12761  ioodisj  12871  fz0fzelfz0  13016  mulexpz  13472  rpexpmord  13535  leexp1a  13542  expmulnbnd  13599  hashf1  13818  fi1uzind  13858  brfi1indALT  13861  swrdccat  14099  reuccatpfxs1  14111  abs3lem  14700  rexanre  14708  cau3lem  14716  limsupgre  14840  limsupbnd2  14842  o1lo1  14896  rlimclim1  14904  rlimclim  14905  rlimcn1  14947  rlimcn2  14949  o1of2  14971  o1rlimmul  14977  lo1add  14985  lo1mul  14986  isercolllem1  15023  climcau  15029  caucvgrlem  15031  caucvgb  15038  summolem2  15075  summo  15076  modfsummod  15151  o1fsum  15170  prodmolem2  15291  addmodlteqALT  15677  rpdvds  16006  isprm5  16053  isprm6  16060  pclem  16177  pcqmul  16192  pcexp  16198  pcneg  16212  pcprmpw2  16220  pcadd  16227  pcmpt  16230  4sqlem13  16295  vdwlem2  16320  vdwlem7  16325  vdwlem12  16330  ramval  16346  ramub2  16352  ramz2  16362  ramcl  16367  cshwshashlem2  16432  imasval  16786  imasdsval  16790  mreexexd  16921  acsfn  16932  issubc3  17121  idfucl  17153  funcres2c  17173  isnat  17219  fucpropd  17249  xpcval  17429  xpcco  17435  prfval  17451  evlf2  17470  evlfcl  17474  curf12  17479  curf1cl  17480  curf2  17481  curfcl  17484  curf2ndf  17499  hof2val  17508  hofcl  17511  hofpropd  17519  yonedalem4a  17527  yonedainv  17533  drsdirfi  17550  pospo  17585  poslubmo  17758  posglbmo  17759  isipodrs  17773  acsinfd  17792  gsumvalx  17888  gsumpropd2lem  17891  ismndd  17935  mndpropd  17938  mhmeql  17992  mndind  17994  frmdup3lem  18033  mhmmnd  18223  issubg4  18300  ssnmz  18320  conjnmzb  18395  f1otrspeq  18577  psgneu  18636  pgpfi  18732  sylow2blem3  18749  slwhash  18751  fislw  18752  sylow3lem2  18755  lsmdisj2  18810  pj1eu  18824  efgredlem  18875  frgpuplem  18900  gexex  18975  frgpnabl  18997  dprdfadd  19144  dpjidcl  19182  pgpfac1lem3  19201  pgpfaclem3  19207  ablfac2  19213  ablsimpgcygd  19230  ablsimpgfind  19234  ablsimpgprmd  19239  ringpropd  19334  islmhm2  19812  lmhmpropd  19847  lbsextlem4  19935  assapropd  20103  psrval  20144  evlslem1  20297  prmirredlem  20642  psgndiflemA  20747  lsmcss  20838  uvcf1  20938  frlmsslsp  20942  frlmup1  20944  mamucl  21012  mamuass  21013  mamudi  21014  mamudir  21015  mamuvs1  21016  mamuvs2  21017  mamulid  21052  mamurid  21053  dmatsubcl  21109  dmatmulcl  21111  scmatscm  21124  marrepval  21173  marepveval  21179  mdetunilem7  21229  gsummatr01lem4  21269  cpmatmcllem  21328  mat2pmatf1  21339  mat2pmatlin  21345  decpmatmul  21382  pm2mpmhmlem2  21429  chpidmat  21457  pptbas  21618  toponmre  21703  restbas  21768  iscncl  21879  cnrest2  21896  cnpdis  21903  lmcnp  21914  dishaus  21992  cmpcovf  22001  tgcmp  22011  dfconn2  22029  clsconn  22040  2ndcctbss  22065  dis2ndc  22070  1stccnp  22072  islly2  22094  cldllycmp  22105  locfincmp  22136  comppfsc  22142  kgentopon  22148  txcls  22214  ptpjopn  22222  dfac14  22228  xkoccn  22229  txcnp  22230  txcmpb  22254  txlm  22258  xkopt  22265  xkoco1cn  22267  xkoco2cn  22268  qtopcn  22324  qtoprest  22327  regr1lem2  22350  xkocnv  22424  qtophmeo  22427  fmfnfmlem4  22567  hausflim  22591  hauspwpwf1  22597  fclscmp  22640  alexsublem  22654  alexsubALTlem2  22658  alexsubALTlem3  22659  ptcmplem3  22664  ptcmplem4  22665  ptcmplem5  22666  cnextfun  22674  tmdgsum2  22706  symgtgp  22716  tsmsval2  22740  tsmsgsum  22749  utoptop  22845  ismet2  22945  blin  23033  metss2lem  23123  methaus  23132  met1stc  23133  met2ndci  23134  prdsxmslem2  23141  metcnp3  23152  metcnpi3  23158  metustto  23165  metustfbas  23169  nlmvscn  23298  nrginvrcn  23303  xrsxmet  23419  reconnlem1  23436  reconn  23438  xrge0tsms  23444  xmetdcn2  23447  metdscn  23466  addcnlem  23474  fsumcn  23480  cnheiborlem  23560  cnheibor  23561  bndth  23564  lebnum  23570  nmoleub2lem2  23722  ipcn  23851  iscmet3  23898  caubl  23913  rrxdstprj1  24014  minveclem3b  24033  minveclem7  24040  pjthlem2  24043  pmltpc  24053  volfiniun  24150  ioombl1  24165  dyadss  24197  dyaddisjlem  24198  dyadmax  24201  dyadmbllem  24202  opnmbllem  24204  itg1addlem2  24300  itg10a  24313  mbfi1fseqlem6  24323  itg2seq  24345  itg2monolem1  24353  itg2gt0  24363  itgfsum  24429  limcfval  24472  ellimc2  24477  ellimc3  24479  limcres  24486  limciun  24494  dvres  24511  dveflem  24578  rolle  24589  dvlip2  24594  c1liplem1  24595  dvgt0lem1  24601  dvgt0  24603  dvlt0  24604  dvne0  24610  dvfsumrlimge0  24629  ftc1lem6  24640  itgsubst  24648  mdegmullem  24674  ply1domn  24719  ply1divex  24732  fta1g  24763  fta1b  24765  plyf  24790  dgrlem  24821  coeid  24830  plydivalg  24890  aannenlem1  24919  aalioulem3  24925  aalioulem6  24928  abelthlem8  25029  efif1olem4  25131  chordthm  25417  xrlimcnp  25548  jensen  25568  lgamcvglem  25619  lgamcvg2  25634  sqf11  25718  fsumvma2  25792  perfectlem2  25808  lgsdilem  25902  lgsquad2lem2  25963  lgsquad3  25965  2sqlem5  26000  2sqlem9  26005  2sqb  26010  rpvmasumlem  26065  dchrisum0flb  26088  dchrisum0  26098  pntpbnd  26166  pntibndlem3  26170  pntleml  26189  tgjustc1  26263  tgjustc2  26264  legov  26373  legtrid  26379  tglinethru  26424  tglnpt2  26429  tglineintmo  26430  mirreu3  26442  perpcom  26501  colperpexlem3  26520  mideu  26526  opphllem1  26535  hlpasch  26544  lnopp2hpgb  26551  trgcopy  26592  brcgr  26688  brbtwn2  26693  colinearalg  26698  axsegcon  26715  axeuclidlem  26750  axcontlem9  26760  ecgrtg  26771  elntg  26772  eengtrkg  26774  upgr1eopALT  26904  usgredg4  27001  subuhgr  27070  subumgr  27072  usgr2wspthon  27746  clwlkclwwlkf1  27790  eupth2lems  28019  n4cyclfrgr  28072  vacn  28473  blocni  28584  ubthlem3  28651  minvecolem7  28662  chocunii  29080  pjhthmo  29081  pjhthlem2  29171  kbass5  29899  mdsymlem5  30186  foresf1o  30267  fcobij  30460  xrofsup  30494  xrge0tsmsd  30694  symgcntz  30731  archirngz  30820  archiabllem2a  30825  isarchiofld  30892  prmidl2  30960  smatrcl  31063  reff  31105  ordtconnlem1  31169  qqhval2  31225  volmeas  31492  fiunelcarsg  31576  ballotlemfc0  31752  ballotlemfcc  31753  signstfvneq0  31844  derangenlem  32420  erdsze2lem1  32452  pconnconn  32480  connpconn  32484  cvxsconn  32492  cvmliftmolem2  32531  cvmliftmo  32533  cvmlift2lem10  32561  cvmlift2lem12  32563  cvmlift3lem7  32574  mrsubff1  32763  msubff1  32805  frpomin  33080  poseq  33097  fprlem2  33140  nolt02o  33201  noprefixmo  33204  nosupbnd2  33218  noetalem3  33221  noetalem5  33223  conway  33266  slerec  33279  ifscgr  33507  cgrxfr  33518  btwnconn1lem13  33562  btwnconn1lem14  33563  outsideofeq  33593  ellines  33615  finminlem  33668  fnejoin2  33719  unbdqndv2  33852  poimirlem13  34907  poimirlem14  34908  poimirlem32  34926  opnmbllem0  34930  mblfinlem3  34933  itg2addnclem  34945  itg2addnc  34948  ftc1cnnc  34968  upixp  35006  filbcmb  35017  sstotbnd2  35054  isbnd3  35064  prdsbnd2  35075  cntotbnd  35076  ismtyima  35083  bfp  35104  rrncmslem  35112  unichnidl  35311  lshpcmp  36126  islshpat  36155  lfl0f  36207  ishlat3N  36492  3dim1  36605  islvol5  36717  lvoli2  36719  lncvrelatN  36919  pclfinclN  37088  pexmidlem8N  37115  idltrn  37288  cdleme42keg  37624  cdleme42mgN  37626  cdlemf2  37700  cdlemg2cex  37729  trlcoat  37861  dihopelvalcpre  38386  dih1dimatlem  38467  dihjatcclem4  38559  lcfl7N  38639  lcfrlem9  38688  mapdh9a  38927  hdmapglem7  39067  renegeulemv  39205  remulinvcom  39255  prjspertr  39262  prjspreln0  39266  nacsfix  39316  mzpsubst  39352  mzpcompact2lem  39355  eldioph2lem2  39365  eldioph2  39366  eldioph2b  39367  diophin  39376  diophun  39377  irrapxlem3  39428  irrapxlem5  39430  pell1234qrreccl  39458  pell1234qrmulcl  39459  pell14qrdich  39473  pell1qrge1  39474  pell1qrgaplem  39477  monotuz  39545  acongtr  39582  acongrep  39584  jm2.23  39600  jm2.26a  39604  jm2.26lem3  39605  jm2.26  39606  jm2.27  39612  wepwsolem  39649  fnwe2lem2  39658  kelac1  39670  kercvrlsm  39690  hbtlem5  39735  hbt  39737  mpaaeu  39757  rfovcnvf1od  40357  mnurndlem1  40624  cncmpmax  41296  rfcnnnub  41300  disjxp1  41338  iccintsng  41806  fprodcn  41888  lptioo2  41919  lptioo1  41920  limclner  41939  stoweidlem31  42323  stoweidlem34  42326  stoweidlem35  42327  stoweidlem49  42341  stoweidlem59  42351  stoweidlem62  42354  fourierdlem60  42458  fourierdlem61  42459  fourierdlem87  42485  iundjiun  42749  ismeannd  42756  hoidmvle  42889  smfsuplem2  43093  2reu8i  43319  prproropf1olem2  43673  paireqne  43680  perfectALTVlem2  43894  mogoldbb  43957  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  isomgrtrlem  44010  mgmhmeql  44077  mndpsuppss  44426  scmsuppss  44427  lindslinindsimp2lem5  44524  elfzolborelfzop1  44581  elbigolo1  44624  itschlc0xyqsol1  44760  itschlc0xyqsol  44761