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

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  994  simp1rr  1094  simp2rr  1098  simp3rr  1102  elpr2elpr  3899  invdisjrab  4122  disjiun  4123  reg2exmidlema  4679  reg3exmidlemwe  4724  nnsucpred  4762  iotam  5367  fvmptt  5794  fcof1  5983  fliftfun  5996  isotr  6016  riotass2  6061  acexmidlemab  6073  ovmpodf  6214  fnmpoovd  6445  1stconst  6451  2ndconst  6452  cnvf1olem  6454  f1od2  6465  suppcofn  6500  smoiso  6567  tfrcldm  6628  tfrcl  6629  nntr2  6770  swoer  6829  erinxp  6877  ecopovsymg  6902  th3qlem1  6905  f1imaen2g  7074  pw2f1odclem  7128  mapdom1g  7141  fict  7164  fidifsnen  7166  dif1enen  7178  fiunsnnn  7179  fisbth  7181  findcard2d  7189  findcard2sd  7190  diffifi  7192  ac6sfi  7196  fimax2gtri  7200  nnwetri  7217  unsnfi  7220  unsnfidcex  7221  unsnfidcel  7222  fisseneq  7236  ssfirab  7238  exmidssfi  7240  fidcenumlemrk  7265  fidcenumlemr  7266  sbthlemi6  7273  sbthlemi8  7275  isbth  7278  fiuni  7306  supmaxti  7338  infminti  7361  ordiso2  7369  eldju2ndl  7406  eldju2ndr  7407  omp1eomlem  7428  difinfsnlem  7433  difinfinf  7435  ctmlemr  7442  ctssdccl  7445  nninfninc  7457  fodjum  7480  fodju0  7481  omniwomnimkv  7501  exmidfodomrlemrALT  7549  acfun  7557  exmidaclem  7558  netap  7614  exmidmotap  7621  ccfunen  7624  cc1  7625  cc2lem  7626  dfplpq2  7715  dfmpq2  7716  mulpipqqs  7734  distrnqg  7748  enq0sym  7793  enq0tr  7795  distrnq0  7820  prarloclem3  7858  genplt2i  7871  addlocpr  7897  prmuloc  7927  distrlem1prl  7943  distrlem1pru  7944  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  ltaprg  7980  prplnqu  7981  addextpr  7982  recexprlemdisj  7991  recexprlemloc  7992  aptiprleml  8000  aptiprlemu  8001  ltmprr  8003  archpr  8004  cauappcvgprlemopl  8007  cauappcvgprlemopu  8009  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlem1  8020  cauappcvgprlemlim  8022  caucvgprlemnkj  8027  caucvgprlemopl  8030  caucvgprlemopu  8032  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprprlemnkltj  8050  caucvgprprlemnkeqj  8051  caucvgprprlemnjltk  8052  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemopu  8060  caucvgprprlemdisj  8063  caucvgprprlemloc  8064  caucvgprprlemaddq  8069  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemex  8083  suplocexprlemub  8084  recexgt0sr  8134  mulgt0sr  8139  prsrriota  8149  suplocsrlem  8169  addcnsr  8195  mulcnsr  8196  mulcnsrec  8204  axmulcom  8232  rereceu  8250  axarch  8252  axcaucvglemres  8260  axpre-suploclemres  8262  lelttr  8408  ltletr  8409  addcan  8500  addcan2  8501  addsub4  8563  ltadd2  8741  le2add  8766  lt2add  8767  lt2sub  8782  le2sub  8783  eqord1  8805  rereim  8908  apreap  8909  apreim  8925  mulreim  8926  apcotr  8929  apadd1  8930  addext  8932  apneg  8933  mulext1  8934  mulext  8936  ltleap  8954  aprcl  8968  mulap0  8976  mulcanapd  8983  recapb  8995  rec11ap  9034  rec11rap  9035  divdivdivap  9037  ddcanap  9050  divadddivap  9051  prodgt0gt0  9175  prodgt0  9176  prodge0  9178  lemulge11  9190  lt2mul2div  9203  ltrec  9207  lerec  9208  lerec2  9213  ledivp1  9227  mulle0r  9268  nn0ge0div  9716  suprzclex  9727  qapne  10022  xrlelttr  10191  xrltletr  10192  xrre3  10207  xrrege0  10210  xaddge0  10263  xle2add  10264  xlt2add  10265  fzass4  10451  fzrev  10474  elfz1b  10480  eluzgtdifelfzo  10598  fzocatel  10600  zsupcllemstep  10645  zsupcllemex  10646  zssinfcl  10648  infssfzcldc  10652  infssfzledc  10653  suprzubdc  10654  exbtwnzlemex  10667  rebtwn2z  10672  modqid  10769  modqcyc  10779  modqaddabs  10782  modqaddmod  10783  mulqaddmodid  10784  modqadd2mod  10794  modqltm1p1mod  10796  modqsubmod  10802  modqsubmodmod  10803  modaddmodup  10807  modqmulmod  10809  modqmulmodr  10810  modqaddmulmod  10811  modqsubdir  10813  frec2uzisod  10827  uzennn  10856  iseqovex  10878  seqvalcd  10881  seq1g  10883  seqf  10884  seqovcd  10887  seqclg  10892  seqm1g  10894  seq3shft2  10901  seqshft2g  10902  monoord  10905  iseqf1olemnab  10921  seqf1oglem1  10939  seqf1og  10941  seqhomog  10950  seqfeq4g  10951  seq3distr  10952  expnegzap  10993  ltexp2a  11011  le2sq2  11035  bernneq  11081  expnlbnd2  11086  nn0ltexp2  11130  nn0opth2  11145  faclbnd  11162  bcval5  11184  hashcl  11203  hashen  11206  fihashdom  11226  hashunlem  11227  hashun  11228  hashxp  11250  hashmap  11251  fimaxq  11253  sseqn  11262  hashfibclem  11265  hashfibc  11266  hashf1lem1  11268  hashf1lem2  11269  hashf1  11270  zfz1isolem1  11275  zfz1iso  11276  seq3coll  11277  sswrd  11296  ccatw2s1p1g  11396  ccatw2s1p2  11397  ccat2s1fstg  11399  wrdind  11477  pfxccatin12lem1  11483  pfxccatin12lem3  11487  reuccatpfxs1lem  11501  cvg1nlemres  11734  cvg1n  11735  resqrexlemp1rp  11755  resqrexlemoverl  11770  resqrexlemex  11774  sqrtsq  11793  abslt  11837  absle  11838  abs3lem  11860  maxleastlt  11964  maxltsup  11967  fimaxre2  11976  negfi  11977  xrmaxleastlt  12005  xrmaxltsup  12007  xrmaxaddlem  12009  2clim  12050  climcn2  12058  addcn2  12059  mulcn2  12061  reccn2ap  12062  climge0  12074  climcau  12096  fzf1o  12125  summodclem2  12132  summodc  12133  zsumdc  12134  fsumf1o  12140  fisumss  12142  fsum3cvg3  12146  fsumcl2lem  12148  fsumadd  12156  mptfzshft  12192  fsumrev  12193  fsummulc2  12198  fsumconst  12204  modfsummod  12208  fsumrelem  12221  binom  12234  cvgratnn  12281  mertenslemub  12284  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodf1o  12338  fprodssdc  12340  fprodmul  12341  fprodcl2lem  12355  fprodrev  12369  fprodconst  12370  fprodap0  12371  fprodrec  12379  fprodap0f  12386  fprodle  12390  fprodmodd  12391  efcllem  12409  tanaddaplem  12488  moddvds  12549  dvdsflip  12601  oexpneg  12627  nn0o  12657  fldivndvdslt  12687  bitsfi  12707  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemeu  12767  dfgcd3  12770  dfgcd2  12774  dvdsmulgcd  12785  bezoutr  12792  nninfctlemfo  12800  lcmgcdlem  12838  coprmdvds2  12854  qredeu  12858  rpdvds  12860  cncongr1  12864  prmind2  12881  isprm5lem  12902  isprm6  12908  oddpwdclemdc  12934  nonsq  12968  hashdvds  12982  crth  12985  eulerthlemh  12992  prmdiveq  12997  hashgcdlem  12999  hashgcdeq  13001  nnnn0modprm0  13017  pclemub  13049  pceu  13057  pcmul  13063  pcqmul  13065  pcgcd1  13090  pc2dvds  13092  difsqpwdvds  13100  pcmpt  13105  prmpwdvds  13117  1arith  13129  mul4sq  13156  4sqlemafi  13157  4sqlemffi  13158  4sqexercise2  13161  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemg  13277  ennnfonelemex  13288  ennnfonelemrnh  13290  ennnfonelemf1  13292  ennnfonelemrn  13293  ennnfonelemdm  13294  ennnfonelemim  13298  ennnfone  13299  ctinf  13304  ctiunctlemfo  13313  nninfdclemcl  13322  nninfdclemf  13323  nninfdclemp1  13324  unbendc  13328  isstruct2r  13346  setscom  13375  ercpbl  13635  opifismgmdc  13674  grpinvalem  13688  gzsumvalx  13692  gzsumfzval  13694  gzsumval2  13697  sgrppropd  13711  mndpropd  13736  issubmnd  13738  submnd0  13740  mhmf1o  13760  subsubm  13773  0mhm  13776  resmhm  13777  mhmco  13780  mhmima  13781  mhmeql  13782  gzsumwsubmcl  13784  gzsumcl  13787  grprcan  13825  grpinvid1  13840  grpinvid2  13841  grplcan  13850  grplmulf1o  13862  grpnpncan0  13884  dfgrp3mlem  13886  grplactcnv  13890  mulgval  13908  mulgfng  13910  mulgnngzsum  13913  mulg1  13915  mulgnnp1  13916  mulgneg  13926  mulgnndir  13937  mulgdirlem  13939  mulgnn0ass  13944  mulgass  13945  subgmulg  13974  issubg4m  13979  subsubg  13983  subgintm  13984  isnsg3  13993  eqgcpbl  14014  ghmeql  14053  ghmnsgima  14054  ghmnsgpreima  14055  ghmf1  14059  ghmf1o  14061  conjghm  14062  qusghm  14068  cmnsubm  14095  ablpncan3  14104  invghm  14116  eqgabl  14117  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gsumvalfi  14135  gsumzfi  14141  gsumclfi  14142  gsummptfidmadd  14144  gsumsubmclfi  14146  gsumconstcmn  14149  prdssgrpd  14174  prdsmndd  14177  pwssub  14199  rngpropd  14237  imasrng  14238  qusrng  14240  srglmhm  14280  srgrmhm  14281  ringpropd  14326  ringlghm  14349  ringrghm  14350  imasring  14352  qusring2  14354  opprrngbg  14366  dvdsrvald  14383  dvdsrd  14384  dvdsrex  14388  dvdsrtr  14391  unitpropdg  14438  rhmopp  14466  isnzr2  14474  issubrng2  14501  subrngintm  14503  subsubrng  14505  subrgintm  14534  subsubrg  14536  rhmpropd  14545  ringunitap  14576  aprap  14581  drngunitap  14591  lmodprop2d  14668  rmodislmod  14671  lssvacl  14685  lssvsubcl  14686  lssvscl  14695  islss3  14699  lss1d  14703  rnglidlmcl  14800  2idlcpblrng  14843  crngridl  14850  gsumfsum  14906  expghmap  14925  mulgghm2  14926  mulgrhm  14927  znf1o  14969  znleval  14971  znidom  14975  znidomb  14976  znunit  14977  asclghm  15008  issubassa2  15018  assamulgscmlem2  15025  psrbagcon  15045  mplsubgfilemcl  15073  iuncld  15199  ssnei2  15241  topssnei  15246  restopnb  15265  cnfval  15278  cnpfval  15279  iscnp4  15302  cnptopco  15306  cncnpi  15312  cncnp  15314  cnconst2  15317  cnrest2  15320  cnptoprest  15323  cnptoprest2  15324  cnpdis  15326  lmss  15330  lmtopcnp  15334  neitx  15352  txcnp  15355  txrest  15360  txdis1cn  15362  txlm  15363  cnmpt21  15375  imasnopn  15383  xmetres2  15463  blvalps  15472  blval  15473  elbl2ps  15476  elbl2  15477  blhalf  15492  blssexps  15513  blssex  15514  ssblex  15515  blin2  15516  bdmetval  15584  xmetxp  15591  xmettx  15594  metcnpi3  15601  txmetcnp  15602  addcncntoplem  15645  fsumcncntop  15651  elcncf2  15658  mulc1cncf  15673  cncfco  15675  cncfmet  15676  cncfmptc  15680  mulcncf  15692  dedekindeulemub  15702  dedekindeulemloc  15703  dedekindeulemlu  15705  dedekindeu  15707  dedekindicclemub  15711  dedekindicclemloc  15712  dedekindicclemlu  15714  dedekindicclemicc  15716  dedekindicc  15717  ivthinclemlopn  15720  ivthinclemuopn  15722  dich0  15736  limcimo  15749  cnplimccntop  15754  limccnp2lem  15760  limccnp2cntop  15761  dvfvalap  15765  dveflem  15810  plycolemc  15842  plyco  15843  plyrecj  15847  reeff1olem  15855  reeff1oleme  15856  eflt  15859  sin0pilem2  15866  pilem3  15867  ioocosf1o  15938  cxplt  16001  cxple  16002  cxplt3  16005  apcxp2  16024  rprelogbmul  16040  rprelogbdiv  16042  logbgt0b  16051  logbgcd1irrap  16055  pellexlem3  16076  mpodvdsmulf1o  16087  fsumdvdsmul  16088  lgsdir2lem5  16134  lgsdi  16139  lgsne0  16140  gausslemma2dlem1f1o  16162  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem2  16184  lgsquad2  16185  2sqlem6  16222  2sqlem8  16225  2sqlem9  16226  2sqlem10  16227  upgredg  16368  usgredg4  16439  uspgredg2vlem  16444  usgr1eop  16469  upgrspanop  16507  umgrspanop  16508  usgrspanop  16509  vtxedgfi  16513  vtxlpfi  16514  iswlkg  16553  upgriswlkdc  16584  upgr2wlkdc  16601  clwwlkccatlem  16624  clwwlknonex2e  16664  nnti  17005  pwtrufal  17010  pwf1oexmid  17012  sssneq  17015  qdencn  17046  cvgcmp2n  17056  trilpolemlt1  17064  trirec0  17067  qdiff  17072  redc0  17081  reap0  17082  cndcap  17083  nconstwlpolemgt0  17088  neap0mkv  17093  supfz  17095  inffz  17096