Theorem simprr 533

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  990  simp1rr  1090  simp2rr  1094  simp3rr  1098  elpr2elpr  3885  invdisjrab  4108  disjiun  4109  reg2exmidlema  4661  reg3exmidlemwe  4706  nnsucpred  4744  iotam  5349  fvmptt  5774  fcof1  5962  fliftfun  5975  isotr  5995  riotass2  6040  acexmidlemab  6052  ovmpodf  6193  fnmpoovd  6424  1stconst  6430  2ndconst  6431  cnvf1olem  6433  f1od2  6444  suppcofn  6479  smoiso  6546  tfrcldm  6607  tfrcl  6608  nntr2  6749  swoer  6808  erinxp  6856  ecopovsymg  6881  th3qlem1  6884  f1imaen2g  7046  pw2f1odclem  7100  mapdom1g  7113  fict  7136  fidifsnen  7138  dif1enen  7150  fiunsnnn  7151  fisbth  7153  findcard2d  7161  findcard2sd  7162  diffifi  7164  ac6sfi  7168  fimax2gtri  7172  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fisseneq  7208  ssfirab  7210  exmidssfi  7212  fidcenumlemrk  7237  fidcenumlemr  7238  sbthlemi6  7245  sbthlemi8  7247  isbth  7250  fiuni  7278  supmaxti  7308  infminti  7331  ordiso2  7339  eldju2ndl  7376  eldju2ndr  7377  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctmlemr  7412  ctssdccl  7415  nninfninc  7427  fodjum  7450  fodju0  7451  omniwomnimkv  7471  exmidfodomrlemrALT  7519  acfun  7527  exmidaclem  7528  netap  7584  exmidmotap  7591  ccfunen  7594  cc1  7595  cc2lem  7596  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  enq0sym  7763  enq0tr  7765  distrnq0  7790  prarloclem3  7828  genplt2i  7841  addlocpr  7867  prmuloc  7897  distrlem1prl  7913  distrlem1pru  7914  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprg  7950  prplnqu  7951  addextpr  7952  recexprlemdisj  7961  recexprlemloc  7962  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  archpr  7974  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemaddq  8039  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  recexgt0sr  8104  mulgt0sr  8109  prsrriota  8119  suplocsrlem  8139  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axmulcom  8202  rereceu  8220  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  addcan  8470  addcan2  8471  addsub4  8533  ltadd2  8711  le2add  8736  lt2add  8737  lt2sub  8752  le2sub  8753  eqord1  8775  rereim  8878  apreap  8879  apreim  8895  mulreim  8896  apcotr  8899  apadd1  8900  addext  8902  apneg  8903  mulext1  8904  mulext  8906  ltleap  8924  aprcl  8938  mulap0  8946  mulcanapd  8953  recapb  8965  rec11ap  9004  rec11rap  9005  divdivdivap  9007  ddcanap  9020  divadddivap  9021  prodgt0gt0  9145  prodgt0  9146  prodge0  9148  lemulge11  9160  lt2mul2div  9173  ltrec  9177  lerec  9178  lerec2  9183  ledivp1  9197  mulle0r  9238  nn0ge0div  9686  suprzclex  9697  qapne  9992  xrlelttr  10161  xrltletr  10162  xrre3  10177  xrrege0  10180  xaddge0  10233  xle2add  10234  xlt2add  10235  fzass4  10420  fzrev  10443  elfz1b  10449  eluzgtdifelfzo  10567  fzocatel  10569  zsupcllemstep  10614  zsupcllemex  10615  zssinfcl  10617  infssfzcldc  10621  infssfzledc  10622  suprzubdc  10623  exbtwnzlemex  10636  rebtwn2z  10641  modqid  10738  modqcyc  10748  modqaddabs  10751  modqaddmod  10752  mulqaddmodid  10753  modqadd2mod  10763  modqltm1p1mod  10765  modqsubmod  10771  modqsubmodmod  10772  modaddmodup  10776  modqmulmod  10778  modqmulmodr  10779  modqaddmulmod  10780  modqsubdir  10782  frec2uzisod  10796  uzennn  10825  iseqovex  10847  seqvalcd  10850  seq1g  10852  seqf  10853  seqovcd  10856  seqclg  10861  seqm1g  10863  seq3shft2  10870  seqshft2g  10871  monoord  10874  iseqf1olemnab  10890  seqf1oglem1  10908  seqf1og  10910  seqhomog  10919  seqfeq4g  10920  seq3distr  10921  expnegzap  10962  ltexp2a  10980  le2sq2  11004  bernneq  11050  expnlbnd2  11055  nn0ltexp2  11099  nn0opth2  11114  faclbnd  11131  bcval5  11153  hashcl  11172  hashen  11175  fihashdom  11195  hashunlem  11196  hashun  11197  hashxp  11219  hashmap  11220  fimaxq  11222  sseqn  11231  hashfibclem  11234  hashfibc  11235  zfz1isolem1  11240  zfz1iso  11241  seq3coll  11242  sswrd  11261  ccatw2s1p1g  11361  ccatw2s1p2  11362  ccat2s1fstg  11364  wrdind  11442  pfxccatin12lem1  11448  pfxccatin12lem3  11452  reuccatpfxs1lem  11466  cvg1nlemres  11698  cvg1n  11699  resqrexlemp1rp  11719  resqrexlemoverl  11734  resqrexlemex  11738  sqrtsq  11757  abslt  11801  absle  11802  abs3lem  11824  maxleastlt  11928  maxltsup  11931  fimaxre2  11940  negfi  11941  xrmaxleastlt  11969  xrmaxltsup  11971  xrmaxaddlem  11973  2clim  12014  climcn2  12022  addcn2  12023  mulcn2  12025  reccn2ap  12026  climge0  12038  climcau  12060  fzf1o  12089  summodclem2  12096  summodc  12097  zsumdc  12098  fsumf1o  12104  fisumss  12106  fsum3cvg3  12110  fsumcl2lem  12112  fsumadd  12120  mptfzshft  12156  fsumrev  12157  fsummulc2  12162  fsumconst  12168  modfsummod  12172  fsumrelem  12185  binom  12198  cvgratnn  12245  mertenslemub  12248  prodmodclem2  12291  prodmodc  12292  zproddc  12293  fprodf1o  12302  fprodssdc  12304  fprodmul  12305  fprodcl2lem  12319  fprodrev  12333  fprodconst  12334  fprodap0  12335  fprodrec  12343  fprodap0f  12350  fprodle  12354  fprodmodd  12355  efcllem  12373  tanaddaplem  12452  moddvds  12513  dvdsflip  12565  oexpneg  12591  nn0o  12621  fldivndvdslt  12651  bitsfi  12671  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemeu  12731  dfgcd3  12734  dfgcd2  12738  dvdsmulgcd  12749  bezoutr  12756  nninfctlemfo  12764  lcmgcdlem  12802  coprmdvds2  12818  qredeu  12822  rpdvds  12824  cncongr1  12828  prmind2  12845  isprm5lem  12866  isprm6  12872  oddpwdclemdc  12898  nonsq  12932  hashdvds  12946  crth  12949  eulerthlemh  12956  prmdiveq  12961  hashgcdlem  12963  hashgcdeq  12965  nnnn0modprm0  12981  pclemub  13013  pceu  13021  pcmul  13027  pcqmul  13029  pcgcd1  13054  pc2dvds  13056  difsqpwdvds  13064  pcmpt  13069  prmpwdvds  13081  1arith  13093  mul4sq  13120  4sqlemafi  13121  4sqlemffi  13122  4sqexercise2  13125  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemg  13241  ennnfonelemex  13252  ennnfonelemrnh  13254  ennnfonelemf1  13256  ennnfonelemrn  13257  ennnfonelemdm  13258  ennnfonelemim  13262  ennnfone  13263  ctinf  13268  ctiunctlemfo  13277  nninfdclemcl  13286  nninfdclemf  13287  nninfdclemp1  13288  unbendc  13292  isstruct2r  13310  setscom  13339  ercpbl  13598  opifismgmdc  13637  grpinvalem  13651  igsumvalx  13655  gsumfzval  13657  gsumval2  13663  sgrppropd  13679  mndpropd  13704  issubmnd  13706  submnd0  13708  mhmf1o  13728  subsubm  13741  0mhm  13744  resmhm  13745  mhmco  13748  mhmima  13749  mhmeql  13750  gsumfzz  13753  gsumwsubmcl  13754  gsumfzcl  13757  grprcan  13795  grpinvid1  13810  grpinvid2  13811  grplcan  13820  grplmulf1o  13832  grpnpncan0  13854  dfgrp3mlem  13856  grplactcnv  13860  mulgval  13878  mulgfng  13880  mulgnngsum  13883  mulg1  13885  mulgnnp1  13886  mulgneg  13896  mulgnndir  13907  mulgdirlem  13909  mulgnn0ass  13914  mulgass  13915  subgmulg  13944  issubg4m  13949  subsubg  13953  subgintm  13954  isnsg3  13963  eqgcpbl  13984  ghmeql  14023  ghmnsgima  14024  ghmnsgpreima  14025  ghmf1  14029  ghmf1o  14031  conjghm  14032  qusghm  14038  ablpncan3  14073  invghm  14085  eqgabl  14086  gsumfzreidx  14093  gsumfzsubmcl  14094  gsumfzmptfidmadd  14095  gsumfzmhm  14099  gfsumval  14105  gfsumz  14112  gfsumcl  14113  prdssgrpd  14136  prdsmndd  14139  pwssub  14161  rngpropd  14197  imasrng  14198  qusrng  14200  srglmhm  14239  srgrmhm  14240  ringpropd  14284  ringlghm  14307  ringrghm  14308  imasring  14310  qusring2  14312  opprrngbg  14324  dvdsrvald  14341  dvdsrd  14342  dvdsrex  14346  dvdsrtr  14349  unitpropdg  14396  rhmopp  14424  isnzr2  14432  issubrng2  14459  subrngintm  14461  subsubrng  14463  subrgintm  14492  subsubrg  14494  rhmpropd  14503  ringunitap  14534  aprap  14539  drngunitap  14549  lmodprop2d  14625  rmodislmod  14628  lssvacl  14642  lssvsubcl  14643  lssvscl  14652  islss3  14656  lss1d  14660  rnglidlmcl  14757  2idlcpblrng  14800  crngridl  14807  expghmap  14884  mulgghm2  14885  mulgrhm  14886  znf1o  14928  znleval  14930  znidom  14934  znidomb  14935  znunit  14936  psrbagcon  14955  mplsubgfilemcl  14983  iuncld  15109  ssnei2  15151  topssnei  15156  restopnb  15175  cnfval  15188  cnpfval  15189  iscnp4  15212  cnptopco  15216  cncnpi  15222  cncnp  15224  cnconst2  15227  cnrest2  15230  cnptoprest  15233  cnptoprest2  15234  cnpdis  15236  lmss  15240  lmtopcnp  15244  neitx  15262  txcnp  15265  txrest  15270  txdis1cn  15272  txlm  15273  cnmpt21  15285  imasnopn  15293  xmetres2  15373  blvalps  15382  blval  15383  elbl2ps  15386  elbl2  15387  blhalf  15402  blssexps  15423  blssex  15424  ssblex  15425  blin2  15426  bdmetval  15494  xmetxp  15501  xmettx  15504  metcnpi3  15511  txmetcnp  15512  addcncntoplem  15555  fsumcncntop  15561  elcncf2  15568  mulc1cncf  15583  cncfco  15585  cncfmet  15586  cncfmptc  15590  mulcncf  15602  dedekindeulemub  15612  dedekindeulemloc  15613  dedekindeulemlu  15615  dedekindeu  15617  dedekindicclemub  15621  dedekindicclemloc  15622  dedekindicclemlu  15624  dedekindicclemicc  15626  dedekindicc  15627  ivthinclemlopn  15630  ivthinclemuopn  15632  dich0  15646  limcimo  15659  cnplimccntop  15664  limccnp2lem  15670  limccnp2cntop  15671  dvfvalap  15675  dveflem  15720  plycolemc  15752  plyco  15753  plyrecj  15757  reeff1olem  15765  reeff1oleme  15766  eflt  15769  sin0pilem2  15776  pilem3  15777  ioocosf1o  15848  cxplt  15910  cxple  15911  cxplt3  15914  apcxp2  15933  rprelogbmul  15949  rprelogbdiv  15951  logbgt0b  15960  logbgcd1irrap  15964  pellexlem3  15976  mpodvdsmulf1o  15987  fsumdvdsmul  15988  lgsdir2lem5  16034  lgsdi  16039  lgsne0  16040  gausslemma2dlem1f1o  16062  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2lem2  16084  lgsquad2  16085  2sqlem6  16122  2sqlem8  16125  2sqlem9  16126  2sqlem10  16127  upgredg  16268  usgredg4  16339  uspgredg2vlem  16344  usgr1eop  16369  upgrspanop  16407  umgrspanop  16408  usgrspanop  16409  vtxedgfi  16413  vtxlpfi  16414  iswlkg  16453  upgriswlkdc  16484  upgr2wlkdc  16501  clwwlkccatlem  16524  clwwlknonex2e  16564  nnti  16905  pwtrufal  16910  pwf1oexmid  16912  sssneq  16915  qdencn  16946  cvgcmp2n  16956  trilpolemlt1  16964  trirec0  16967  qdiff  16972  redc0  16981  reap0  16982  cndcap  16983  nconstwlpolemgt0  16989  neap0mkv  16994  supfz  16996  inffz  16997