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:  dfifp2dc  987  simp1rr  1087  simp2rr  1091  simp3rr  1095  elpr2elpr  3854  invdisjrab  4077  disjiun  4078  reg2exmidlema  4627  reg3exmidlemwe  4672  nnsucpred  4710  iotam  5313  fvmptt  5731  fcof1  5916  fliftfun  5929  isotr  5949  riotass2  5992  acexmidlemab  6004  ovmpodf  6145  fnmpoovd  6372  1stconst  6378  2ndconst  6379  cnvf1olem  6381  f1od2  6392  smoiso  6459  tfrcldm  6520  tfrcl  6521  nntr2  6662  swoer  6721  erinxp  6769  ecopovsymg  6794  th3qlem1  6797  f1imaen2g  6958  pw2f1odclem  7008  mapdom1g  7021  fict  7043  fidifsnen  7045  dif1enen  7055  fiunsnnn  7056  fisbth  7058  findcard2d  7066  findcard2sd  7067  diffifi  7069  ac6sfi  7073  fimax2gtri  7077  nnwetri  7094  unsnfi  7097  unsnfidcex  7098  unsnfidcel  7099  fisseneq  7112  ssfirab  7114  fidcenumlemrk  7137  fidcenumlemr  7138  sbthlemi6  7145  sbthlemi8  7147  isbth  7150  fiuni  7161  supmaxti  7187  infminti  7210  ordiso2  7218  eldju2ndl  7255  eldju2ndr  7256  omp1eomlem  7277  difinfsnlem  7282  difinfinf  7284  ctmlemr  7291  ctssdccl  7294  nninfninc  7306  fodjum  7329  fodju0  7330  omniwomnimkv  7350  exmidfodomrlemrALT  7397  acfun  7405  exmidaclem  7406  netap  7456  exmidmotap  7463  ccfunen  7466  cc1  7467  cc2lem  7468  dfplpq2  7557  dfmpq2  7558  mulpipqqs  7576  distrnqg  7590  enq0sym  7635  enq0tr  7637  distrnq0  7662  prarloclem3  7700  genplt2i  7713  addlocpr  7739  prmuloc  7769  distrlem1prl  7785  distrlem1pru  7786  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  ltaprg  7822  prplnqu  7823  addextpr  7824  recexprlemdisj  7833  recexprlemloc  7834  aptiprleml  7842  aptiprlemu  7843  ltmprr  7845  archpr  7846  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlem1  7862  cauappcvgprlemlim  7864  caucvgprlemnkj  7869  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprprlemnkltj  7892  caucvgprprlemnkeqj  7893  caucvgprprlemnjltk  7894  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemopu  7902  caucvgprprlemdisj  7905  caucvgprprlemloc  7906  caucvgprprlemaddq  7911  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemex  7925  suplocexprlemub  7926  recexgt0sr  7976  mulgt0sr  7981  prsrriota  7991  suplocsrlem  8011  addcnsr  8037  mulcnsr  8038  mulcnsrec  8046  axmulcom  8074  rereceu  8092  axarch  8094  axcaucvglemres  8102  axpre-suploclemres  8104  lelttr  8251  ltletr  8252  addcan  8342  addcan2  8343  addsub4  8405  ltadd2  8582  le2add  8607  lt2add  8608  lt2sub  8623  le2sub  8624  eqord1  8646  rereim  8749  apreap  8750  apreim  8766  mulreim  8767  apcotr  8770  apadd1  8771  addext  8773  apneg  8774  mulext1  8775  mulext  8777  ltleap  8795  aprcl  8809  mulap0  8817  mulcanapd  8824  recapb  8834  rec11ap  8873  rec11rap  8874  divdivdivap  8876  ddcanap  8889  divadddivap  8890  prodgt0gt0  9014  prodgt0  9015  prodge0  9017  lemulge11  9029  lt2mul2div  9042  ltrec  9046  lerec  9047  lerec2  9052  ledivp1  9066  mulle0r  9107  nn0ge0div  9550  suprzclex  9561  qapne  9851  xrlelttr  10019  xrltletr  10020  xrre3  10035  xrrege0  10038  xaddge0  10091  xle2add  10092  xlt2add  10093  fzass4  10275  fzrev  10297  elfz1b  10303  eluzgtdifelfzo  10420  fzocatel  10422  zsupcllemstep  10466  zsupcllemex  10467  zssinfcl  10469  suprzubdc  10473  exbtwnzlemex  10486  rebtwn2z  10491  modqid  10588  modqcyc  10598  modqaddabs  10601  modqaddmod  10602  mulqaddmodid  10603  modqadd2mod  10613  modqltm1p1mod  10615  modqsubmod  10621  modqsubmodmod  10622  modaddmodup  10626  modqmulmod  10628  modqmulmodr  10629  modqaddmulmod  10630  modqsubdir  10632  frec2uzisod  10646  uzennn  10675  iseqovex  10697  seqvalcd  10700  seq1g  10702  seqf  10703  seqovcd  10706  seqclg  10711  seqm1g  10713  seq3shft2  10720  seqshft2g  10721  monoord  10724  iseqf1olemnab  10740  seqf1oglem1  10758  seqf1og  10760  seqhomog  10769  seqfeq4g  10770  seq3distr  10771  expnegzap  10812  ltexp2a  10830  le2sq2  10854  bernneq  10899  expnlbnd2  10904  nn0ltexp2  10948  nn0opth2  10963  faclbnd  10980  bcval5  11002  hashcl  11020  hashen  11023  fihashdom  11042  hashunlem  11043  hashun  11044  hashxp  11066  fimaxq  11067  zfz1isolem1  11080  zfz1iso  11081  seq3coll  11082  sswrd  11098  ccatw2s1p2  11197  wrdind  11275  pfxccatin12lem1  11281  pfxccatin12lem3  11285  reuccatpfxs1lem  11299  cvg1nlemres  11517  cvg1n  11518  resqrexlemp1rp  11538  resqrexlemoverl  11553  resqrexlemex  11557  sqrtsq  11576  abslt  11620  absle  11621  abs3lem  11643  maxleastlt  11747  maxltsup  11750  fimaxre2  11759  negfi  11760  xrmaxleastlt  11788  xrmaxltsup  11790  xrmaxaddlem  11792  2clim  11833  climcn2  11841  addcn2  11842  mulcn2  11844  reccn2ap  11845  climge0  11857  climcau  11879  summodclem2  11914  summodc  11915  zsumdc  11916  fsumf1o  11922  fisumss  11924  fsum3cvg3  11928  fsumcl2lem  11930  fsumadd  11938  mptfzshft  11974  fsumrev  11975  fsummulc2  11980  fsumconst  11986  modfsummod  11990  fsumrelem  12003  binom  12016  cvgratnn  12063  mertenslemub  12066  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodf1o  12120  fprodssdc  12122  fprodmul  12123  fprodcl2lem  12137  fprodrev  12151  fprodconst  12152  fprodap0  12153  fprodrec  12161  fprodap0f  12168  fprodle  12172  fprodmodd  12173  efcllem  12191  tanaddaplem  12270  moddvds  12331  dvdsflip  12383  oexpneg  12409  nn0o  12439  fldivndvdslt  12469  bitsfi  12489  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemeu  12549  dfgcd3  12552  dfgcd2  12556  dvdsmulgcd  12567  bezoutr  12574  nninfctlemfo  12582  lcmgcdlem  12620  coprmdvds2  12636  qredeu  12640  rpdvds  12642  cncongr1  12646  prmind2  12663  isprm5lem  12684  isprm6  12690  oddpwdclemdc  12716  nonsq  12750  hashdvds  12764  crth  12767  eulerthlemh  12774  prmdiveq  12779  hashgcdlem  12781  hashgcdeq  12783  nnnn0modprm0  12799  pclemub  12831  pceu  12839  pcmul  12845  pcqmul  12847  pcgcd1  12872  pc2dvds  12874  difsqpwdvds  12882  pcmpt  12887  prmpwdvds  12899  1arith  12911  mul4sq  12938  4sqlemafi  12939  4sqlemffi  12940  4sqexercise2  12943  ennnfonelemg  12995  ennnfonelemex  13006  ennnfonelemrnh  13008  ennnfonelemf1  13010  ennnfonelemrn  13011  ennnfonelemdm  13012  ennnfonelemim  13016  ennnfone  13017  ctinf  13022  ctiunctlemfo  13031  nninfdclemcl  13040  nninfdclemf  13041  nninfdclemp1  13042  unbendc  13046  isstruct2r  13064  setscom  13093  ercpbl  13385  opifismgmdc  13425  grpinvalem  13439  igsumvalx  13443  gsumfzval  13445  gsumval2  13451  sgrppropd  13467  prdssgrpd  13469  mndpropd  13494  issubmnd  13496  submnd0  13498  prdsmndd  13502  mhmf1o  13524  subsubm  13537  0mhm  13540  resmhm  13541  mhmco  13544  mhmima  13545  mhmeql  13546  gsumfzz  13549  gsumwsubmcl  13550  gsumfzcl  13553  grprcan  13591  grpinvid1  13606  grpinvid2  13607  grplcan  13616  grplmulf1o  13628  grpnpncan0  13650  dfgrp3mlem  13652  grplactcnv  13656  pwssub  13667  mulgval  13680  mulgfng  13682  mulgnngsum  13685  mulg1  13687  mulgnnp1  13688  mulgneg  13698  mulgnndir  13709  mulgdirlem  13711  mulgnn0ass  13716  mulgass  13717  subgmulg  13746  issubg4m  13751  subsubg  13755  subgintm  13756  isnsg3  13765  eqgcpbl  13786  ghmeql  13825  ghmnsgima  13826  ghmnsgpreima  13827  ghmf1  13831  ghmf1o  13833  conjghm  13834  qusghm  13840  ablpncan3  13875  invghm  13887  eqgabl  13888  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  rngpropd  13939  imasrng  13940  qusrng  13942  srglmhm  13977  srgrmhm  13978  ringpropd  14022  ringlghm  14045  ringrghm  14046  imasring  14048  qusring2  14050  opprrngbg  14062  dvdsrvald  14078  dvdsrd  14079  dvdsrex  14083  dvdsrtr  14086  unitpropdg  14133  rhmopp  14161  isnzr2  14169  issubrng2  14195  subrngintm  14197  subsubrng  14199  subrgintm  14228  subsubrg  14230  rhmpropd  14239  aprap  14271  lmodprop2d  14333  rmodislmod  14336  lssvacl  14350  lssvsubcl  14351  lssvscl  14360  islss3  14364  lss1d  14368  rnglidlmcl  14465  2idlcpblrng  14508  crngridl  14515  expghmap  14592  mulgghm2  14593  mulgrhm  14594  znf1o  14636  znleval  14638  znidom  14642  znidomb  14643  znunit  14644  mplsubgfilemcl  14684  iuncld  14810  ssnei2  14852  topssnei  14857  restopnb  14876  cnfval  14889  cnpfval  14890  iscnp4  14913  cnptopco  14917  cncnpi  14923  cncnp  14925  cnconst2  14928  cnrest2  14931  cnptoprest  14934  cnptoprest2  14935  cnpdis  14937  lmss  14941  lmtopcnp  14945  neitx  14963  txcnp  14966  txrest  14971  txdis1cn  14973  txlm  14974  cnmpt21  14986  imasnopn  14994  xmetres2  15074  blvalps  15083  blval  15084  elbl2ps  15087  elbl2  15088  blhalf  15103  blssexps  15124  blssex  15125  ssblex  15126  blin2  15127  bdmetval  15195  xmetxp  15202  xmettx  15205  metcnpi3  15212  txmetcnp  15213  addcncntoplem  15256  fsumcncntop  15262  elcncf2  15269  mulc1cncf  15284  cncfco  15286  cncfmet  15287  cncfmptc  15291  mulcncf  15303  dedekindeulemub  15313  dedekindeulemloc  15314  dedekindeulemlu  15316  dedekindeu  15318  dedekindicclemub  15322  dedekindicclemloc  15323  dedekindicclemlu  15325  dedekindicclemicc  15327  dedekindicc  15328  ivthinclemlopn  15331  ivthinclemuopn  15333  dich0  15347  limcimo  15360  cnplimccntop  15365  limccnp2lem  15371  limccnp2cntop  15372  dvfvalap  15376  dveflem  15421  plycolemc  15453  plyco  15454  plyrecj  15458  reeff1olem  15466  reeff1oleme  15467  eflt  15470  sin0pilem2  15477  pilem3  15478  ioocosf1o  15549  cxplt  15611  cxple  15612  cxplt3  15615  apcxp2  15634  rprelogbmul  15650  rprelogbdiv  15652  logbgt0b  15661  logbgcd1irrap  15665  mpodvdsmulf1o  15685  fsumdvdsmul  15686  lgsdir2lem5  15732  lgsdi  15737  lgsne0  15738  gausslemma2dlem1f1o  15760  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem2  15782  lgsquad2  15783  2sqlem6  15820  2sqlem8  15823  2sqlem9  15824  2sqlem10  15825  upgredg  15963  usgredg4  16034  uspgredg2vlem  16039  usgr1eop  16064  vtxedgfi  16075  vtxlpfi  16076  iswlkg  16101  upgriswlkdc  16132  upgr2wlkdc  16147  clwwlkccatlem  16169  nnti  16469  pwtrufal  16476  pwf1oexmid  16478  sssneq  16481  qdencn  16509  cvgcmp2n  16515  trilpolemlt1  16523  trirec0  16526  redc0  16539  reap0  16540  cndcap  16541  nconstwlpolemgt0  16546  neap0mkv  16551  supfz  16553  inffz  16554