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:  simp1rr  1063  simp2rr  1067  simp3rr  1071  disjiun  3993  reg2exmidlema  4527  reg3exmidlemwe  4572  nnsucpred  4610  iotam  5200  fvmptt  5599  fcof1  5774  fliftfun  5787  isotr  5807  riotass2  5847  acexmidlemab  5859  ovmpodf  5996  fnmpoovd  6206  1stconst  6212  2ndconst  6213  cnvf1olem  6215  f1od2  6226  smoiso  6293  tfrcldm  6354  tfrcl  6355  nntr2  6494  swoer  6553  erinxp  6599  ecopovsymg  6624  th3qlem1  6627  f1imaen2g  6783  mapdom1g  6837  fict  6858  fidifsnen  6860  dif1enen  6870  fiunsnnn  6871  fisbth  6873  findcard2d  6881  findcard2sd  6882  diffifi  6884  ac6sfi  6888  fimax2gtri  6891  nnwetri  6905  unsnfi  6908  unsnfidcex  6909  unsnfidcel  6910  fisseneq  6921  ssfirab  6923  fidcenumlemrk  6943  fidcenumlemr  6944  sbthlemi6  6951  sbthlemi8  6953  isbth  6956  fiuni  6967  supmaxti  6993  infminti  7016  ordiso2  7024  eldju2ndl  7061  eldju2ndr  7062  omp1eomlem  7083  difinfsnlem  7088  difinfinf  7090  ctmlemr  7097  ctssdccl  7100  fodjum  7134  fodju0  7135  omniwomnimkv  7155  exmidfodomrlemrALT  7192  acfun  7196  exmidaclem  7197  ccfunen  7238  cc1  7239  cc2lem  7240  dfplpq2  7328  dfmpq2  7329  mulpipqqs  7347  distrnqg  7361  enq0sym  7406  enq0tr  7408  distrnq0  7433  prarloclem3  7471  genplt2i  7484  addlocpr  7510  prmuloc  7540  distrlem1prl  7556  distrlem1pru  7557  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  ltaprg  7593  prplnqu  7594  addextpr  7595  recexprlemdisj  7604  recexprlemloc  7605  aptiprleml  7613  aptiprlemu  7614  ltmprr  7616  archpr  7617  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlem1  7633  cauappcvgprlemlim  7635  caucvgprlemnkj  7640  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnjltk  7665  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemdisj  7676  caucvgprprlemloc  7677  caucvgprprlemaddq  7682  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  recexgt0sr  7747  mulgt0sr  7752  prsrriota  7762  suplocsrlem  7782  addcnsr  7808  mulcnsr  7809  mulcnsrec  7817  axmulcom  7845  rereceu  7863  axarch  7865  axcaucvglemres  7873  axpre-suploclemres  7875  lelttr  8020  ltletr  8021  addcan  8111  addcan2  8112  addsub4  8174  ltadd2  8350  le2add  8375  lt2add  8376  lt2sub  8391  le2sub  8392  eqord1  8414  rereim  8517  apreap  8518  apreim  8534  mulreim  8535  apcotr  8538  apadd1  8539  addext  8541  apneg  8542  mulext1  8543  mulext  8545  ltleap  8563  aprcl  8577  mulap0  8584  mulcanapd  8591  rec11ap  8639  rec11rap  8640  divdivdivap  8642  ddcanap  8655  divadddivap  8656  prodgt0gt0  8779  prodgt0  8780  prodge0  8782  lemulge11  8794  lt2mul2div  8807  ltrec  8811  lerec  8812  lerec2  8817  ledivp1  8831  mulle0r  8872  nn0ge0div  9311  suprzclex  9322  qapne  9610  xrlelttr  9775  xrltletr  9776  xrre3  9791  xrrege0  9794  xaddge0  9847  xle2add  9848  xlt2add  9849  fzass4  10030  fzrev  10052  elfz1b  10058  eluzgtdifelfzo  10165  fzocatel  10167  exbtwnzlemex  10218  rebtwn2z  10223  modqid  10317  modqcyc  10327  modqaddabs  10330  modqaddmod  10331  mulqaddmodid  10332  modqadd2mod  10342  modqltm1p1mod  10344  modqsubmod  10350  modqsubmodmod  10351  modaddmodup  10355  modqmulmod  10357  modqmulmodr  10358  modqaddmulmod  10359  modqsubdir  10361  frec2uzisod  10375  uzennn  10404  iseqovex  10424  seqvalcd  10427  seqf  10429  seqovcd  10431  seq3shft2  10441  monoord  10444  iseqf1olemnab  10456  seq3distr  10481  expnegzap  10522  ltexp2a  10540  le2sq2  10563  bernneq  10608  expnlbnd2  10613  nn0ltexp2  10656  nn0opth2  10670  faclbnd  10687  bcval5  10709  hashcl  10727  hashen  10730  fihashdom  10749  hashunlem  10750  hashun  10751  hashxp  10772  fimaxq  10773  zfz1isolem1  10786  zfz1iso  10787  seq3coll  10788  cvg1nlemres  10960  cvg1n  10961  resqrexlemp1rp  10981  resqrexlemoverl  10996  resqrexlemex  11000  sqrtsq  11019  abslt  11063  absle  11064  abs3lem  11086  maxleastlt  11190  maxltsup  11193  fimaxre2  11201  negfi  11202  xrmaxleastlt  11230  xrmaxltsup  11232  xrmaxaddlem  11234  2clim  11275  climcn2  11283  addcn2  11284  mulcn2  11286  reccn2ap  11287  climge0  11299  climcau  11321  summodclem2  11356  summodc  11357  zsumdc  11358  fsumf1o  11364  fisumss  11366  fsum3cvg3  11370  fsumcl2lem  11372  fsumadd  11380  mptfzshft  11416  fsumrev  11417  fsummulc2  11422  fsumconst  11428  modfsummod  11432  fsumrelem  11445  binom  11458  cvgratnn  11505  mertenslemub  11508  prodmodclem2  11551  prodmodc  11552  zproddc  11553  fprodf1o  11562  fprodssdc  11564  fprodmul  11565  fprodcl2lem  11579  fprodrev  11593  fprodconst  11594  fprodap0  11595  fprodrec  11603  fprodap0f  11610  fprodle  11614  fprodmodd  11615  efcllem  11633  tanaddaplem  11712  moddvds  11772  dvdsflip  11822  oexpneg  11847  nn0o  11877  fldivndvdslt  11905  zsupcllemstep  11911  zsupcllemex  11912  zssinfcl  11914  suprzubdc  11918  bezoutlemnewy  11962  bezoutlemstep  11963  bezoutlemeu  11973  dfgcd3  11976  dfgcd2  11980  dvdsmulgcd  11991  bezoutr  11998  lcmgcdlem  12042  coprmdvds2  12058  qredeu  12062  rpdvds  12064  cncongr1  12068  prmind2  12085  isprm5lem  12106  isprm6  12112  oddpwdclemdc  12138  nonsq  12172  hashdvds  12186  crth  12189  eulerthlemh  12196  prmdiveq  12201  hashgcdlem  12203  hashgcdeq  12204  nnnn0modprm0  12220  pclemub  12252  pceu  12260  pcmul  12266  pcqmul  12268  pcgcd1  12292  pc2dvds  12294  difsqpwdvds  12302  pcmpt  12306  prmpwdvds  12318  1arith  12330  mul4sq  12357  ennnfonelemg  12369  ennnfonelemex  12380  ennnfonelemrnh  12382  ennnfonelemf1  12384  ennnfonelemrn  12385  ennnfonelemdm  12386  ennnfonelemim  12390  ennnfone  12391  ctinf  12396  ctiunctlemfo  12405  nninfdclemcl  12414  nninfdclemf  12415  nninfdclemp1  12416  unbendc  12420  isstruct2r  12438  setscom  12467  opifismgmdc  12654  grprinvlem  12668  mndpropd  12705  mhmf1o  12722  0mhm  12733  mhmco  12734  mhmima  12735  mhmeql  12736  grprcan  12770  grpinvid1  12784  grpinvid2  12785  grplcan  12791  grplmulf1o  12803  grpnpncan0  12825  dfgrp3mlem  12827  grplactcnv  12831  mulgval  12845  mulgfng  12846  mulg1  12849  mulgnnp1  12850  mulgneg  12860  mulgnndir  12870  mulgdirlem  12872  mulgnn0ass  12877  mulgass  12878  ablpncan3  12916  srglmhm  12969  srgrmhm  12970  ringpropd  13009  iuncld  13166  ssnei2  13208  topssnei  13213  restopnb  13232  cnfval  13245  cnpfval  13246  iscnp4  13269  cnptopco  13273  cncnpi  13279  cncnp  13281  cnconst2  13284  cnrest2  13287  cnptoprest  13290  cnptoprest2  13291  cnpdis  13293  lmss  13297  lmtopcnp  13301  neitx  13319  txcnp  13322  txrest  13327  txdis1cn  13329  txlm  13330  cnmpt21  13342  imasnopn  13350  xmetres2  13430  blvalps  13439  blval  13440  elbl2ps  13443  elbl2  13444  blhalf  13459  blssexps  13480  blssex  13481  ssblex  13482  blin2  13483  bdmetval  13551  xmetxp  13558  xmettx  13561  metcnpi3  13568  txmetcnp  13569  addcncntoplem  13602  fsumcncntop  13607  elcncf2  13612  mulc1cncf  13627  cncfco  13629  cncfmet  13630  cncfmptc  13633  mulcncf  13642  dedekindeulemub  13647  dedekindeulemloc  13648  dedekindeulemlu  13650  dedekindeu  13652  dedekindicclemub  13656  dedekindicclemloc  13657  dedekindicclemlu  13659  dedekindicclemicc  13661  dedekindicc  13662  ivthinclemlopn  13665  ivthinclemuopn  13667  limcimo  13685  cnplimccntop  13690  limccnp2lem  13696  limccnp2cntop  13697  dvfvalap  13701  dveflem  13738  reeff1olem  13743  reeff1oleme  13744  eflt  13747  sin0pilem2  13754  pilem3  13755  ioocosf1o  13826  cxplt  13887  cxple  13888  cxplt3  13891  apcxp2  13909  rprelogbmul  13924  rprelogbdiv  13926  logbgt0b  13935  logbgcd1irrap  13939  lgsdir2lem5  13984  lgsdi  13989  lgsne0  13990  2sqlem6  14007  2sqlem8  14010  2sqlem9  14011  2sqlem10  14012  nnti  14284  pwtrufal  14287  pwf1oexmid  14289  sssneq  14292  qdencn  14316  cvgcmp2n  14322  trilpolemlt1  14330  trirec0  14333  redc0  14346  reap0  14347  nconstwlpolemgt0  14352  supfz  14357  inffz  14358