Theorem simprr 531

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2	1	ad2antll 491	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1rr  1065  simp2rr  1069  simp3rr  1073  disjiun  4029  reg2exmidlema  4571  reg3exmidlemwe  4616  nnsucpred  4654  iotam  5251  fvmptt  5656  fcof1  5833  fliftfun  5846  isotr  5866  riotass2  5907  acexmidlemab  5919  ovmpodf  6058  fnmpoovd  6282  1stconst  6288  2ndconst  6289  cnvf1olem  6291  f1od2  6302  smoiso  6369  tfrcldm  6430  tfrcl  6431  nntr2  6570  swoer  6629  erinxp  6677  ecopovsymg  6702  th3qlem1  6705  f1imaen2g  6861  pw2f1odclem  6904  mapdom1g  6917  fict  6938  fidifsnen  6940  dif1enen  6950  fiunsnnn  6951  fisbth  6953  findcard2d  6961  findcard2sd  6962  diffifi  6964  ac6sfi  6968  fimax2gtri  6971  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  ssfirab  7006  fidcenumlemrk  7029  fidcenumlemr  7030  sbthlemi6  7037  sbthlemi8  7039  isbth  7042  fiuni  7053  supmaxti  7079  infminti  7102  ordiso2  7110  eldju2ndl  7147  eldju2ndr  7148  omp1eomlem  7169  difinfsnlem  7174  difinfinf  7176  ctmlemr  7183  ctssdccl  7186  nninfninc  7198  fodjum  7221  fodju0  7222  omniwomnimkv  7242  exmidfodomrlemrALT  7284  acfun  7292  exmidaclem  7293  netap  7339  exmidmotap  7346  ccfunen  7349  cc1  7350  cc2lem  7351  dfplpq2  7440  dfmpq2  7441  mulpipqqs  7459  distrnqg  7473  enq0sym  7518  enq0tr  7520  distrnq0  7545  prarloclem3  7583  genplt2i  7596  addlocpr  7622  prmuloc  7652  distrlem1prl  7668  distrlem1pru  7669  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  ltaprg  7705  prplnqu  7706  addextpr  7707  recexprlemdisj  7716  recexprlemloc  7717  aptiprleml  7725  aptiprlemu  7726  ltmprr  7728  archpr  7729  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlem1  7745  cauappcvgprlemlim  7747  caucvgprlemnkj  7752  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemdisj  7788  caucvgprprlemloc  7789  caucvgprprlemaddq  7794  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  recexgt0sr  7859  mulgt0sr  7864  prsrriota  7874  suplocsrlem  7894  addcnsr  7920  mulcnsr  7921  mulcnsrec  7929  axmulcom  7957  rereceu  7975  axarch  7977  axcaucvglemres  7985  axpre-suploclemres  7987  lelttr  8134  ltletr  8135  addcan  8225  addcan2  8226  addsub4  8288  ltadd2  8465  le2add  8490  lt2add  8491  lt2sub  8506  le2sub  8507  eqord1  8529  rereim  8632  apreap  8633  apreim  8649  mulreim  8650  apcotr  8653  apadd1  8654  addext  8656  apneg  8657  mulext1  8658  mulext  8660  ltleap  8678  aprcl  8692  mulap0  8700  mulcanapd  8707  recapb  8717  rec11ap  8756  rec11rap  8757  divdivdivap  8759  ddcanap  8772  divadddivap  8773  prodgt0gt0  8897  prodgt0  8898  prodge0  8900  lemulge11  8912  lt2mul2div  8925  ltrec  8929  lerec  8930  lerec2  8935  ledivp1  8949  mulle0r  8990  nn0ge0div  9432  suprzclex  9443  qapne  9732  xrlelttr  9900  xrltletr  9901  xrre3  9916  xrrege0  9919  xaddge0  9972  xle2add  9973  xlt2add  9974  fzass4  10156  fzrev  10178  elfz1b  10184  eluzgtdifelfzo  10292  fzocatel  10294  zsupcllemstep  10338  zsupcllemex  10339  zssinfcl  10341  suprzubdc  10345  exbtwnzlemex  10358  rebtwn2z  10363  modqid  10460  modqcyc  10470  modqaddabs  10473  modqaddmod  10474  mulqaddmodid  10475  modqadd2mod  10485  modqltm1p1mod  10487  modqsubmod  10493  modqsubmodmod  10494  modaddmodup  10498  modqmulmod  10500  modqmulmodr  10501  modqaddmulmod  10502  modqsubdir  10504  frec2uzisod  10518  uzennn  10547  iseqovex  10569  seqvalcd  10572  seq1g  10574  seqf  10575  seqovcd  10578  seqclg  10583  seqm1g  10585  seq3shft2  10592  seqshft2g  10593  monoord  10596  iseqf1olemnab  10612  seqf1oglem1  10630  seqf1og  10632  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  expnegzap  10684  ltexp2a  10702  le2sq2  10726  bernneq  10771  expnlbnd2  10776  nn0ltexp2  10820  nn0opth2  10835  faclbnd  10852  bcval5  10874  hashcl  10892  hashen  10895  fihashdom  10914  hashunlem  10915  hashun  10916  hashxp  10937  fimaxq  10938  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  sswrd  10963  cvg1nlemres  11169  cvg1n  11170  resqrexlemp1rp  11190  resqrexlemoverl  11205  resqrexlemex  11209  sqrtsq  11228  abslt  11272  absle  11273  abs3lem  11295  maxleastlt  11399  maxltsup  11402  fimaxre2  11411  negfi  11412  xrmaxleastlt  11440  xrmaxltsup  11442  xrmaxaddlem  11444  2clim  11485  climcn2  11493  addcn2  11494  mulcn2  11496  reccn2ap  11497  climge0  11509  climcau  11531  summodclem2  11566  summodc  11567  zsumdc  11568  fsumf1o  11574  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  mptfzshft  11626  fsumrev  11627  fsummulc2  11632  fsumconst  11638  modfsummod  11642  fsumrelem  11655  binom  11668  cvgratnn  11715  mertenslemub  11718  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  fprodcl2lem  11789  fprodrev  11803  fprodconst  11804  fprodap0  11805  fprodrec  11813  fprodap0f  11820  fprodle  11824  fprodmodd  11825  efcllem  11843  tanaddaplem  11922  moddvds  11983  dvdsflip  12035  oexpneg  12061  nn0o  12091  fldivndvdslt  12121  bitsfi  12141  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemeu  12201  dfgcd3  12204  dfgcd2  12208  dvdsmulgcd  12219  bezoutr  12226  nninfctlemfo  12234  lcmgcdlem  12272  coprmdvds2  12288  qredeu  12292  rpdvds  12294  cncongr1  12298  prmind2  12315  isprm5lem  12336  isprm6  12342  oddpwdclemdc  12368  nonsq  12402  hashdvds  12416  crth  12419  eulerthlemh  12426  prmdiveq  12431  hashgcdlem  12433  hashgcdeq  12435  nnnn0modprm0  12451  pclemub  12483  pceu  12491  pcmul  12497  pcqmul  12499  pcgcd1  12524  pc2dvds  12526  difsqpwdvds  12534  pcmpt  12539  prmpwdvds  12551  1arith  12563  mul4sq  12590  4sqlemafi  12591  4sqlemffi  12592  4sqexercise2  12595  ennnfonelemg  12647  ennnfonelemex  12658  ennnfonelemrnh  12660  ennnfonelemf1  12662  ennnfonelemrn  12663  ennnfonelemdm  12664  ennnfonelemim  12668  ennnfone  12669  ctinf  12674  ctiunctlemfo  12683  nninfdclemcl  12692  nninfdclemf  12693  nninfdclemp1  12694  unbendc  12698  isstruct2r  12716  setscom  12745  ercpbl  13035  opifismgmdc  13075  grpinvalem  13089  igsumvalx  13093  gsumfzval  13095  gsumval2  13101  sgrppropd  13117  prdssgrpd  13119  mndpropd  13144  issubmnd  13146  submnd0  13148  prdsmndd  13152  mhmf1o  13174  subsubm  13187  0mhm  13190  resmhm  13191  mhmco  13194  mhmima  13195  mhmeql  13196  gsumfzz  13199  gsumwsubmcl  13200  gsumfzcl  13203  grprcan  13241  grpinvid1  13256  grpinvid2  13257  grplcan  13266  grplmulf1o  13278  grpnpncan0  13300  dfgrp3mlem  13302  grplactcnv  13306  pwssub  13317  mulgval  13330  mulgfng  13332  mulgnngsum  13335  mulg1  13337  mulgnnp1  13338  mulgneg  13348  mulgnndir  13359  mulgdirlem  13361  mulgnn0ass  13366  mulgass  13367  subgmulg  13396  issubg4m  13401  subsubg  13405  subgintm  13406  isnsg3  13415  eqgcpbl  13436  ghmeql  13475  ghmnsgima  13476  ghmnsgpreima  13477  ghmf1  13481  ghmf1o  13483  conjghm  13484  qusghm  13490  ablpncan3  13525  invghm  13537  eqgabl  13538  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  rngpropd  13589  imasrng  13590  qusrng  13592  srglmhm  13627  srgrmhm  13628  ringpropd  13672  ringlghm  13695  ringrghm  13696  imasring  13698  qusring2  13700  opprrngbg  13712  dvdsrvald  13727  dvdsrd  13728  dvdsrex  13732  dvdsrtr  13735  unitpropdg  13782  rhmopp  13810  isnzr2  13818  issubrng2  13844  subrngintm  13846  subsubrng  13848  subrgintm  13877  subsubrg  13879  rhmpropd  13888  aprap  13920  lmodprop2d  13982  rmodislmod  13985  lssvacl  13999  lssvsubcl  14000  lssvscl  14009  islss3  14013  lss1d  14017  rnglidlmcl  14114  2idlcpblrng  14157  crngridl  14164  expghmap  14241  mulgghm2  14242  mulgrhm  14243  znf1o  14285  znleval  14287  znidom  14291  znidomb  14292  znunit  14293  iuncld  14437  ssnei2  14479  topssnei  14484  restopnb  14503  cnfval  14516  cnpfval  14517  iscnp4  14540  cnptopco  14544  cncnpi  14550  cncnp  14552  cnconst2  14555  cnrest2  14558  cnptoprest  14561  cnptoprest2  14562  cnpdis  14564  lmss  14568  lmtopcnp  14572  neitx  14590  txcnp  14593  txrest  14598  txdis1cn  14600  txlm  14601  cnmpt21  14613  imasnopn  14621  xmetres2  14701  blvalps  14710  blval  14711  elbl2ps  14714  elbl2  14715  blhalf  14730  blssexps  14751  blssex  14752  ssblex  14753  blin2  14754  bdmetval  14822  xmetxp  14829  xmettx  14832  metcnpi3  14839  txmetcnp  14840  addcncntoplem  14883  fsumcncntop  14889  elcncf2  14896  mulc1cncf  14911  cncfco  14913  cncfmet  14914  cncfmptc  14918  mulcncf  14930  dedekindeulemub  14940  dedekindeulemloc  14941  dedekindeulemlu  14943  dedekindeu  14945  dedekindicclemub  14949  dedekindicclemloc  14950  dedekindicclemlu  14952  dedekindicclemicc  14954  dedekindicc  14955  ivthinclemlopn  14958  ivthinclemuopn  14960  dich0  14974  limcimo  14987  cnplimccntop  14992  limccnp2lem  14998  limccnp2cntop  14999  dvfvalap  15003  dveflem  15048  plycolemc  15080  plyco  15081  plyrecj  15085  reeff1olem  15093  reeff1oleme  15094  eflt  15097  sin0pilem2  15104  pilem3  15105  ioocosf1o  15176  cxplt  15238  cxple  15239  cxplt3  15242  apcxp2  15261  rprelogbmul  15277  rprelogbdiv  15279  logbgt0b  15288  logbgcd1irrap  15292  mpodvdsmulf1o  15312  fsumdvdsmul  15313  lgsdir2lem5  15359  lgsdi  15364  lgsne0  15365  gausslemma2dlem1f1o  15387  lgseisenlem2  15398  lgsquadlem1  15404  lgsquadlem2  15405  lgsquadlem3  15406  lgsquad2lem2  15409  lgsquad2  15410  2sqlem6  15447  2sqlem8  15450  2sqlem9  15451  2sqlem10  15452  nnti  15725  pwtrufal  15730  pwf1oexmid  15732  sssneq  15735  qdencn  15762  cvgcmp2n  15768  trilpolemlt1  15776  trirec0  15779  redc0  15792  reap0  15793  cndcap  15794  nconstwlpolemgt0  15799  neap0mkv  15804  supfz  15806  inffz  15807