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  4681  reg3exmidlemwe  4726  nnsucpred  4764  iotam  5369  fvmptt  5797  fcof1  5989  fliftfun  6002  isotr  6022  riotass2  6067  acexmidlemab  6079  ovmpodf  6220  fnmpoovd  6451  1stconst  6457  2ndconst  6458  cnvf1olem  6460  f1od2  6471  suppcofn  6506  smoiso  6573  tfrcldm  6634  tfrcl  6635  nntr2  6776  swoer  6835  erinxp  6883  ecopovsymg  6908  th3qlem1  6911  f1imaen2g  7080  pw2f1odclem  7134  mapdom1g  7147  fict  7170  fidifsnen  7172  dif1enen  7184  fiunsnnn  7185  fisbth  7187  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fimax2gtri  7206  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  ssfirab  7244  exmidssfi  7246  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlemi6  7279  sbthlemi8  7281  isbth  7284  fiuni  7312  supmaxti  7344  infminti  7367  ordiso2  7375  eldju2ndl  7412  eldju2ndr  7413  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctmlemr  7448  ctssdccl  7451  nninfninc  7463  fodjum  7486  fodju0  7487  omniwomnimkv  7507  exmidfodomrlemrALT  7555  acfun  7563  exmidaclem  7564  netap  7620  exmidmotap  7627  ccfunen  7630  cc1  7631  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  enq0sym  7799  enq0tr  7801  distrnq0  7826  prarloclem3  7864  genplt2i  7877  addlocpr  7903  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprg  7986  prplnqu  7987  addextpr  7988  recexprlemdisj  7997  recexprlemloc  7998  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  recexgt0sr  8140  mulgt0sr  8145  prsrriota  8155  suplocsrlem  8175  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axmulcom  8238  rereceu  8256  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  addcan  8506  addcan2  8507  addsub4  8569  ltadd2  8747  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  eqord1  8811  rereim  8915  apreap  8916  apreim  8932  mulreim  8933  apcotr  8936  apadd1  8937  addext  8939  apneg  8940  mulext1  8941  mulext  8943  ltleap  8961  aprcl  8975  mulap0  8983  mulcanapd  8990  recapb  9002  rec11ap  9041  rec11rap  9042  divdivdivap  9044  ddcanap  9057  divadddivap  9058  prodgt0gt0  9182  prodgt0  9183  prodge0  9185  lemulge11  9197  lt2mul2div  9210  ltrec  9214  lerec  9215  lerec2  9220  ledivp1  9234  mulle0r  9275  nn0ge0div  9735  suprzclex  9746  qapne  10041  xrlelttr  10210  xrltletr  10211  xrre3  10226  xrrege0  10229  xaddge0  10282  xle2add  10283  xlt2add  10284  fzass4  10470  fzrev  10493  elfz1b  10499  eluzgtdifelfzo  10617  fzocatel  10619  zsupcllemstep  10664  zsupcllemex  10665  zssinfcl  10667  infssfzcldc  10671  infssfzledc  10672  suprzubdc  10673  exbtwnzlemex  10686  rebtwn2z  10691  modqid  10788  modqcyc  10798  modqaddabs  10801  modqaddmod  10802  mulqaddmodid  10803  modqadd2mod  10813  modqltm1p1mod  10815  modqsubmod  10821  modqsubmodmod  10822  modaddmodup  10826  modqmulmod  10828  modqmulmodr  10829  modqaddmulmod  10830  modqsubdir  10832  frec2uzisod  10846  uzennn  10875  iseqovex  10897  seqvalcd  10900  seq1g  10902  seqf  10903  seqovcd  10906  seqclg  10911  seqm1g  10913  seq3shft2  10920  seqshft2g  10921  monoord  10924  iseqf1olemnab  10940  seqf1oglem1  10958  seqf1og  10960  seqhomog  10969  seqfeq4g  10970  seq3distr  10971  expnegzap  11012  ltexp2a  11030  le2sq2  11054  bernneq  11100  expnlbnd2  11105  nn0ltexp2  11149  nn0opth2  11164  faclbnd  11181  bcval5  11203  hashcl  11222  hashen  11225  fihashdom  11245  hashunlem  11246  hashun  11247  hashxp  11269  hashmap  11270  fimaxq  11272  sseqn  11281  hashfibclem  11284  hashfibc  11285  hashf1lem1  11287  hashf1lem2  11288  hashf1  11289  zfz1isolem1  11294  zfz1iso  11295  seq3coll  11296  sswrd  11315  ccatw2s1p1g  11415  ccatw2s1p2  11416  ccat2s1fstg  11418  wrdind  11496  pfxccatin12lem1  11502  pfxccatin12lem3  11506  reuccatpfxs1lem  11520  cvg1nlemres  11753  cvg1n  11754  resqrexlemp1rp  11774  resqrexlemoverl  11789  resqrexlemex  11793  sqrtsq  11812  abslt  11856  absle  11857  abs3lem  11879  maxleastlt  11983  maxltsup  11986  fimaxre2  11995  negfi  11996  xrmaxleastlt  12024  xrmaxltsup  12026  xrmaxaddlem  12028  2clim  12069  climcn2  12077  addcn2  12078  mulcn2  12080  reccn2ap  12081  climge0  12093  climcau  12115  fzf1o  12144  summodclem2  12151  summodc  12152  zsumdc  12153  fsumf1o  12159  fisumss  12161  fsum3cvg3  12165  fsumcl2lem  12167  fsumadd  12175  mptfzshft  12211  fsumrev  12212  fsummulc2  12217  fsumconst  12223  modfsummod  12227  fsumrelem  12240  binom  12253  cvgratnn  12300  mertenslemub  12303  prodmodclem2  12346  prodmodc  12347  zproddc  12348  fprodf1o  12357  fprodssdc  12359  fprodmul  12360  fprodcl2lem  12374  fprodrev  12388  fprodconst  12389  fprodap0  12390  fprodrec  12398  fprodap0f  12405  fprodle  12409  fprodmodd  12410  efcllem  12428  tanaddaplem  12507  moddvds  12568  dvdsflip  12620  oexpneg  12646  nn0o  12676  fldivndvdslt  12706  bitsfi  12726  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemeu  12786  dfgcd3  12789  dfgcd2  12793  dvdsmulgcd  12804  bezoutr  12811  nninfctlemfo  12819  lcmgcdlem  12857  coprmdvds2  12873  qredeu  12877  rpdvds  12879  cncongr1  12883  prmind2  12900  isprm5lem  12921  isprm6  12927  oddpwdclemdc  12953  nonsq  12987  hashdvds  13001  crth  13004  eulerthlemh  13011  prmdiveq  13016  hashgcdlem  13018  hashgcdeq  13020  nnnn0modprm0  13036  pclemub  13068  pceu  13076  pcmul  13082  pcqmul  13084  pcgcd1  13109  pc2dvds  13111  difsqpwdvds  13119  pcmpt  13124  prmpwdvds  13136  1arith  13148  mul4sq  13175  4sqlemafi  13176  4sqlemffi  13177  4sqexercise2  13180  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemg  13296  ennnfonelemex  13307  ennnfonelemrnh  13309  ennnfonelemf1  13311  ennnfonelemrn  13312  ennnfonelemdm  13313  ennnfonelemim  13317  ennnfone  13318  ctinf  13323  ctiunctlemfo  13332  nninfdclemcl  13341  nninfdclemf  13342  nninfdclemp1  13343  unbendc  13347  isstruct2r  13365  setscom  13394  ercpbl  13654  opifismgmdc  13693  grpinvalem  13707  gzsumvalx  13711  gzsumfzval  13713  gzsumval2  13716  sgrppropd  13730  mndpropd  13755  issubmnd  13757  submnd0  13759  mhmf1o  13779  subsubm  13792  0mhm  13795  resmhm  13796  mhmco  13799  mhmima  13800  mhmeql  13801  gzsumwsubmcl  13803  gzsumcl  13806  grprcan  13844  grpinvid1  13859  grpinvid2  13860  grplcan  13869  grplmulf1o  13881  grpnpncan0  13903  dfgrp3mlem  13905  grplactcnv  13909  mulgval  13927  mulgfng  13929  mulgnngzsum  13932  mulg1  13934  mulgnnp1  13935  mulgneg  13945  mulgnndir  13956  mulgdirlem  13958  mulgnn0ass  13963  mulgass  13964  subgmulg  13993  issubg4m  13998  subsubg  14002  subgintm  14003  isnsg3  14012  eqgcpbl  14033  ghmeql  14072  ghmnsgima  14073  ghmnsgpreima  14074  ghmf1  14078  ghmf1o  14080  conjghm  14081  qusghm  14087  cmnsubm  14114  ablpncan3  14123  invghm  14135  eqgabl  14136  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gsumvalfi  14154  gsumzfi  14160  gsumclfi  14161  gsummptfidmadd  14163  gsumsubmclfi  14165  gsumconstcmn  14168  prdssgrpd  14193  prdsmndd  14196  pwssub  14218  rngpropd  14256  imasrng  14257  qusrng  14259  srglmhm  14299  srgrmhm  14300  ringpropd  14345  ringlghm  14368  ringrghm  14369  imasring  14371  qusring2  14373  opprrngbg  14385  dvdsrvald  14402  dvdsrd  14403  dvdsrex  14407  dvdsrtr  14410  unitpropdg  14457  rhmopp  14485  isnzr2  14493  issubrng2  14520  subrngintm  14522  subsubrng  14524  subrgintm  14553  subsubrg  14555  rhmpropd  14564  ringunitap  14595  aprap  14600  drngunitap  14610  lmodprop2d  14687  rmodislmod  14690  lssvacl  14704  lssvsubcl  14705  lssvscl  14714  islss3  14718  lss1d  14722  rnglidlmcl  14819  2idlcpblrng  14862  crngridl  14869  gsumfsum  14925  expghmap  14944  mulgghm2  14945  mulgrhm  14946  znf1o  14988  znleval  14990  znidom  14994  znidomb  14995  znunit  14996  asclghm  15027  issubassa2  15037  assamulgscmlem2  15044  psrbagcon  15064  mplsubgfilemcl  15092  iuncld  15218  ssnei2  15260  topssnei  15265  restopnb  15284  cnfval  15297  cnpfval  15298  iscnp4  15321  cnptopco  15325  cncnpi  15331  cncnp  15333  cnconst2  15336  cnrest2  15339  cnptoprest  15342  cnptoprest2  15343  cnpdis  15345  lmss  15349  lmtopcnp  15353  neitx  15371  txcnp  15374  txrest  15379  txdis1cn  15381  txlm  15382  cnmpt21  15394  imasnopn  15402  xmetres2  15482  blvalps  15491  blval  15492  elbl2ps  15495  elbl2  15496  blhalf  15511  blssexps  15532  blssex  15533  ssblex  15534  blin2  15535  bdmetval  15603  xmetxp  15610  xmettx  15613  metcnpi3  15620  txmetcnp  15621  addcncntoplem  15664  fsumcncntop  15670  elcncf2  15677  mulc1cncf  15692  cncfco  15694  cncfmet  15695  cncfmptc  15699  mulcncf  15711  dedekindeulemub  15721  dedekindeulemloc  15722  dedekindeulemlu  15724  dedekindeu  15726  dedekindicclemub  15730  dedekindicclemloc  15731  dedekindicclemlu  15733  dedekindicclemicc  15735  dedekindicc  15736  ivthinclemlopn  15739  ivthinclemuopn  15741  dich0  15755  limcimo  15768  cnplimccntop  15773  limccnp2lem  15779  limccnp2cntop  15780  dvfvalap  15784  dveflem  15829  plycolemc  15861  plyco  15862  plyrecj  15866  reeff1olem  15874  reeff1oleme  15875  eflt  15878  sin0pilem2  15886  pilem3  15887  ioocosf1o  15958  logdivlt  15999  logdivle  16000  cxplt  16024  cxple  16025  cxplt3  16028  apcxp2  16047  rprelogbmul  16063  rprelogbdiv  16065  logbgt0b  16074  logbgcd1irrap  16078  pellexlem3  16099  mpodvdsmulf1o  16110  fsumdvdsmul  16111  lgsdir2lem5  16163  lgsdi  16168  lgsne0  16169  gausslemma2dlem1f1o  16191  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem2  16213  lgsquad2  16214  2sqlem6  16251  2sqlem8  16254  2sqlem9  16255  2sqlem10  16256  upgredg  16397  usgredg4  16468  uspgredg2vlem  16473  usgr1eop  16498  upgrspanop  16536  umgrspanop  16537  usgrspanop  16538  vtxedgfi  16542  vtxlpfi  16543  iswlkg  16582  upgriswlkdc  16613  upgr2wlkdc  16630  clwwlkccatlem  16653  clwwlknonex2e  16693  nnti  17034  pwtrufal  17039  pwf1oexmid  17041  sssneq  17044  qdencn  17084  cvgcmp2n  17094  trilpolemlt1  17102  trirec0  17105  qdiff  17110  redc0  17119  reap0  17120  cndcap  17121  nconstwlpolemgt0  17126  neap0mkv  17131  supfz  17133  inffz  17134