Theorem simprr 537

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 495	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dfifp2dc  994  simp1rr  1094  simp2rr  1098  simp3rr  1102  elpr2elpr  3901  invdisjrab  4124  disjiun  4125  reg2exmidlema  4683  reg3exmidlemwe  4728  nnsucpred  4766  iotam  5372  fvmptt  5800  fcof1  5992  fliftfun  6005  isotr  6025  riotass2  6070  acexmidlemab  6082  ovmpodf  6223  fnmpoovd  6455  1stconst  6461  2ndconst  6462  cnvf1olem  6464  f1od2  6475  suppcofn  6510  smoiso  6577  tfrcldm  6638  tfrcl  6639  nntr2  6780  swoer  6839  erinxp  6887  ecopovsymg  6912  th3qlem1  6915  f1imaen2g  7085  pw2f1odclem  7139  mapdom1g  7152  fict  7175  fidifsnen  7177  dif1enen  7189  fiunsnnn  7190  fisbth  7192  findcard2d  7200  findcard2sd  7201  diffifi  7203  ac6sfi  7207  fimax2gtri  7211  nnwetri  7228  unsnfi  7231  unsnfidcex  7232  unsnfidcel  7233  fisseneq  7247  ssfirab  7249  exmidssfi  7251  fidcenumlemrk  7277  fidcenumlemr  7278  sbthlemi6  7285  sbthlemi8  7287  isbth  7290  fiuni  7318  supmaxti  7351  infminti  7374  ordiso2  7382  eldju2ndl  7419  eldju2ndr  7420  omp1eomlem  7441  difinfsnlem  7446  difinfinf  7448  ctmlemr  7455  ctssdccl  7458  nninfninc  7470  fodjum  7493  fodju0  7494  omniwomnimkv  7514  exmidfodomrlemrALT  7562  acfun  7570  exmidaclem  7571  netap  7627  exmidmotap  7634  ccfunen  7637  cc1  7638  cc2lem  7639  dfplpq2  7728  dfmpq2  7729  mulpipqqs  7747  distrnqg  7761  enq0sym  7806  enq0tr  7808  distrnq0  7833  prarloclem3  7871  genplt2i  7884  addlocpr  7910  prmuloc  7940  distrlem1prl  7956  distrlem1pru  7957  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  ltaprg  7993  prplnqu  7994  addextpr  7995  recexprlemdisj  8004  recexprlemloc  8005  aptiprleml  8013  aptiprlemu  8014  ltmprr  8016  archpr  8017  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlem1  8033  cauappcvgprlemlim  8035  caucvgprlemnkj  8040  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprprlemnkltj  8063  caucvgprprlemnkeqj  8064  caucvgprprlemnjltk  8065  caucvgprprlemml  8068  caucvgprprlemmu  8069  caucvgprprlemopl  8071  caucvgprprlemopu  8073  caucvgprprlemdisj  8076  caucvgprprlemloc  8077  caucvgprprlemaddq  8082  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemex  8096  suplocexprlemub  8097  recexgt0sr  8147  mulgt0sr  8152  prsrriota  8162  suplocsrlem  8182  addcnsr  8208  mulcnsr  8209  mulcnsrec  8217  axmulcom  8245  rereceu  8263  axarch  8265  axcaucvglemres  8273  axpre-suploclemres  8275  lelttr  8421  ltletr  8422  addcan  8514  addcan2  8515  addsub4  8577  ltadd2  8755  le2add  8780  lt2add  8781  lt2sub  8796  le2sub  8797  eqord1  8819  rereim  8923  apreap  8924  apreim  8940  mulreim  8941  apcotr  8944  apadd1  8945  addext  8947  apneg  8948  mulext1  8949  mulext  8951  ltleap  8969  aprcl  8983  mulap0  8991  mulcanapd  8998  recapb  9010  rec11ap  9049  rec11rap  9050  divdivdivap  9052  ddcanap  9065  divadddivap  9066  prodgt0gt0  9190  prodgt0  9191  prodge0  9193  lemulge11  9205  lt2mul2div  9218  ltrec  9222  lerec  9223  lerec2  9228  ledivp1  9242  mulle0r  9283  nn0ge0div  9745  suprzclex  9756  qapne  10056  xrlelttr  10226  xrltletr  10227  xrre3  10242  xrrege0  10245  xaddge0  10298  xle2add  10299  xlt2add  10300  fzass4  10486  fzrev  10509  elfz1b  10515  eluzgtdifelfzo  10633  fzocatel  10635  zsupcllemstep  10680  zsupcllemex  10681  zssinfcl  10683  infssfzcldc  10687  infssfzledc  10688  suprzubdc  10689  exbtwnzlemex  10702  rebtwn2z  10707  modqid  10808  modqcyc  10818  modqaddabs  10821  modqaddmod  10822  mulqaddmodid  10823  modqadd2mod  10833  modqltm1p1mod  10835  modqsubmod  10841  modqsubmodmod  10842  modaddmodup  10846  modqmulmod  10848  modqmulmodr  10849  modqaddmulmod  10850  modqsubdir  10852  frec2uzisod  10866  uzennn  10895  iseqovex  10917  seqvalcd  10920  seq1g  10922  seqf  10923  seqovcd  10926  seqclg  10931  seqm1g  10933  seq3shft2  10940  seqshft2g  10941  monoord  10944  iseqf1olemnab  10960  seqf1oglem1  10978  seqf1og  10980  seqhomog  10989  seqfeq4g  10990  seq3distr  10991  expnegzap  11032  ltexp2a  11050  le2sq2  11074  bernneq  11120  expnlbnd2  11125  nn0ltexp2  11170  nn0opth2  11185  faclbnd  11202  bcval5  11224  hashcl  11243  hashen  11246  fihashdom  11266  hashunlem  11267  hashun  11268  hashxp  11290  hashmap  11291  fimaxq  11293  sseqn  11302  hashfibclem  11305  hashfibc  11306  hashf1lem1  11308  hashf1lem2  11309  hashf1  11310  zfz1isolem1  11315  zfz1iso  11316  seq3coll  11317  sswrd  11336  ccatw2s1p1g  11436  ccatw2s1p2  11437  ccat2s1fstg  11439  wrdind  11517  pfxccatin12lem1  11523  pfxccatin12lem3  11527  reuccatpfxs1lem  11541  cvg1nlemres  11774  cvg1n  11775  resqrexlemp1rp  11795  resqrexlemoverl  11810  resqrexlemex  11814  sqrtsq  11833  abslt  11878  absle  11879  abs3lem  11901  maxleastlt  12005  maxltsup  12008  fimaxre2  12017  negfi  12018  fiidxsupcl  12019  xrmaxleastlt  12048  xrmaxltsup  12050  xrmaxaddlem  12052  2clim  12093  climcn2  12101  addcn2  12102  mulcn2  12104  reccn2ap  12105  climge0  12117  climcau  12139  fzf1o  12168  summodclem2  12175  summodc  12176  zsumdc  12177  fsumf1o  12183  fisumss  12185  fsum3cvg3  12189  fsumcl2lem  12191  fsumadd  12199  mptfzshft  12235  fsumrev  12236  fsummulc2  12241  fsumconst  12247  modfsummod  12251  fsumrelem  12264  binom  12277  cvgratnn  12324  mertenslemub  12327  prodmodclem2  12370  prodmodc  12371  zproddc  12372  fprodf1o  12381  fprodssdc  12383  fprodmul  12384  fprodcl2lem  12398  fprodrev  12412  fprodconst  12413  fprodap0  12414  fprodrec  12422  fprodap0f  12429  fprodle  12433  fprodmodd  12434  efcllem  12452  tanaddaplem  12531  moddvds  12592  dvdsflip  12644  oexpneg  12670  nn0o  12700  fldivndvdslt  12730  bitsfi  12750  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemeu  12810  dfgcd3  12813  dfgcd2  12817  dvdsmulgcd  12828  bezoutr  12835  nninfctlemfo  12843  lcmgcdlem  12881  coprmdvds2  12897  qredeu  12901  rpdvds  12903  cncongr1  12907  prmind2  12924  isprm5lem  12946  isprm6  12952  nnmaxpwlemparts  12978  nnmaxpw  12979  nonsq  13013  nn0sqdcq  13014  sqrtrirr  13015  hashdvds  13029  crth  13032  eulerthlemh  13039  prmdiveq  13044  hashgcdlem  13046  hashgcdeq  13048  nnnn0modprm0  13064  pclemub  13096  pceu  13104  pcmul  13110  pcqmul  13112  pcgcd1  13137  pc2dvds  13139  difsqpwdvds  13147  pcmpt  13152  prmpwdvds  13164  1arith  13176  mul4sq  13203  4sqlemafi  13204  4sqlemffi  13205  4sqexercise2  13208  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemg  13353  ennnfonelemex  13364  ennnfonelemrnh  13366  ennnfonelemf1  13368  ennnfonelemrn  13369  ennnfonelemdm  13370  ennnfonelemim  13374  ennnfone  13375  ctinf  13380  ctiunctlemfo  13389  nninfdclemcl  13398  nninfdclemf  13399  nninfdclemp1  13400  unbendc  13404  isstruct2r  13422  setscom  13451  ercpbl  13712  opifismgmdc  13751  grpinvalem  13765  gzsumvalx  13769  gzsumfzval  13771  gzsumval2  13774  sgrppropd  13788  mndpropd  13813  issubmnd  13815  submnd0  13817  mhmf1o  13837  subsubm  13850  0mhm  13853  resmhm  13854  mhmco  13857  mhmima  13858  mhmeql  13859  gzsumwsubmcl  13861  gzsumcl  13864  grprcan  13902  grpinvid1  13917  grpinvid2  13918  grplcan  13927  grplmulf1o  13939  grpnpncan0  13961  dfgrp3mlem  13963  grplactcnv  13967  mulgval  13985  mulgfng  13987  mulgnngzsum  13990  mulg1  13992  mulgnnp1  13993  mulgneg  14003  mulgnndir  14014  mulgdirlem  14016  mulgnn0ass  14021  mulgass  14022  subgmulg  14051  issubg4m  14056  subsubg  14060  subgintm  14061  isnsg3  14070  eqgcpbl  14091  ghmeql  14130  ghmnsgima  14131  ghmnsgpreima  14132  ghmf1  14136  ghmf1o  14138  conjghm  14139  qusghm  14145  cntzsgrpcl  14168  cntzsubm  14171  cntrsubgnsg  14176  cmnsubm  14203  ablpncan3  14212  invghm  14224  eqgabl  14225  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gsumvalfi  14243  gsumzfi  14249  gsumclfi  14250  gsummptfidmadd  14252  gsumsubmclfi  14254  gsummptfidmsplit  14255  gsumresfi  14264  gsumconstcmn  14267  gsum2dfilem2  14273  gsum2d2fi  14275  prdssgrpd  14299  prdsmndd  14302  pwssub  14324  rngpropd  14362  imasrng  14363  qusrng  14365  srglmhm  14405  srgrmhm  14406  ringpropd  14451  ringlghm  14474  ringrghm  14475  imasring  14479  qusring2  14481  opprrngbg  14493  dvdsrvald  14510  dvdsrd  14511  dvdsrex  14515  dvdsrtr  14518  unitpropdg  14565  rhmopp  14593  isnzr2  14601  issubrng2  14628  subrngintm  14630  subsubrng  14632  subrgintm  14661  subsubrg  14663  rhmpropd  14672  ringunitap  14703  aprap  14708  drngunitap  14718  lmodprop2d  14795  rmodislmod  14798  lssvacl  14812  lssvsubcl  14813  lssvscl  14822  islss3  14826  lss1d  14830  rnglidlmcl  14927  2idlcpblrng  14970  crngridl  14977  gsumfsum  15033  expghmap  15052  mulgghm2  15053  mulgrhm  15054  znf1o  15096  znleval  15098  znidom  15102  znidomb  15103  znunit  15104  asclghm  15135  issubassa2  15145  assamulgscmlem2  15152  psrbagcon  15176  psrbaglefifi  15177  gsumbagdiaglem  15180  mplsubgfilemcl  15227  iuncld  15353  ssnei2  15395  topssnei  15400  restopnb  15419  cnfval  15432  cnpfval  15433  iscnp4  15456  cnptopco  15460  cncnpi  15466  cncnp  15468  cnconst2  15471  cnrest2  15474  cnptoprest  15477  cnptoprest2  15478  cnpdis  15480  lmss  15484  lmtopcnp  15488  neitx  15506  txcnp  15509  txrest  15514  txdis1cn  15516  txlm  15517  cnmpt21  15529  imasnopn  15537  xmetres2  15617  blvalps  15626  blval  15627  elbl2ps  15630  elbl2  15631  blhalf  15646  blssexps  15667  blssex  15668  ssblex  15669  blin2  15670  bdmetval  15738  xmetxp  15745  xmettx  15748  metcnpi3  15755  txmetcnp  15756  addcncntoplem  15799  fsumcncntop  15805  elcncf2  15812  mulc1cncf  15827  cncfco  15829  cncfmet  15830  cncfmptc  15834  mulcncf  15846  dedekindeulemub  15856  dedekindeulemloc  15857  dedekindeulemlu  15859  dedekindeu  15861  dedekindicclemub  15865  dedekindicclemloc  15866  dedekindicclemlu  15868  dedekindicclemicc  15870  dedekindicc  15871  ivthinclemlopn  15874  ivthinclemuopn  15876  dich0  15890  limcimo  15903  cnplimccntop  15908  limccnp2lem  15914  limccnp2cntop  15915  dvfvalap  15919  dveflem  15964  plycolemc  15996  plyco  15997  plyrecj  16001  reeff1olem  16009  reeff1oleme  16010  eflt  16013  sin0pilem2  16021  pilem3  16022  ioocosf1o  16094  logdivlt  16136  logdivle  16137  rpcxpmul2z  16160  cxplt  16163  cxple  16164  cxplt3  16167  apcxp2  16186  rprelogbmul  16203  rprelogbdiv  16205  logbgt0b  16214  logbgcd1irrap  16218  zprmlogbap  16230  pellexlem3  16243  ppinprm  16272  chtnprm  16274  mpodvdsmulf1o  16296  fsumdvdsmul  16297  chtublem  16307  bposlem3  16325  lgsdir2lem5  16368  lgsdi  16373  lgsne0  16374  gausslemma2dlem1f1o  16396  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2lem2  16418  lgsquad2  16419  2sqlem6  16456  2sqlem8  16459  2sqlem9  16460  2sqlem10  16461  upgredg  16602  usgredg4  16673  uspgredg2vlem  16678  usgr1eop  16703  upgrspanop  16741  umgrspanop  16742  usgrspanop  16743  vtxedgfi  16747  vtxlpfi  16748  iswlkg  16787  upgriswlkdc  16818  upgr2wlkdc  16835  clwwlkccatlem  16858  clwwlknonex2e  16898  nnti  17239  pwtrufal  17244  pwf1oexmid  17246  sssneq  17249  qdencn  17290  cvgcmp2n  17300  trilpolemlt1  17309  trirec0  17312  qdiff  17317  redc0  17326  reap0  17327  cndcap  17328  nconstwlpolemgt0  17333  neap0mkv  17338  supfz  17340  inffz  17341