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  3999  reg2exmidlema  4534  reg3exmidlemwe  4579  nnsucpred  4617  iotam  5209  fvmptt  5608  fcof1  5784  fliftfun  5797  isotr  5817  riotass2  5857  acexmidlemab  5869  ovmpodf  6006  fnmpoovd  6216  1stconst  6222  2ndconst  6223  cnvf1olem  6225  f1od2  6236  smoiso  6303  tfrcldm  6364  tfrcl  6365  nntr2  6504  swoer  6563  erinxp  6609  ecopovsymg  6634  th3qlem1  6637  f1imaen2g  6793  mapdom1g  6847  fict  6868  fidifsnen  6870  dif1enen  6880  fiunsnnn  6881  fisbth  6883  findcard2d  6891  findcard2sd  6892  diffifi  6894  ac6sfi  6898  fimax2gtri  6901  nnwetri  6915  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  fisseneq  6931  ssfirab  6933  fidcenumlemrk  6953  fidcenumlemr  6954  sbthlemi6  6961  sbthlemi8  6963  isbth  6966  fiuni  6977  supmaxti  7003  infminti  7026  ordiso2  7034  eldju2ndl  7071  eldju2ndr  7072  omp1eomlem  7093  difinfsnlem  7098  difinfinf  7100  ctmlemr  7107  ctssdccl  7110  fodjum  7144  fodju0  7145  omniwomnimkv  7165  exmidfodomrlemrALT  7202  acfun  7206  exmidaclem  7207  netap  7253  exmidmotap  7260  ccfunen  7263  cc1  7264  cc2lem  7265  dfplpq2  7353  dfmpq2  7354  mulpipqqs  7372  distrnqg  7386  enq0sym  7431  enq0tr  7433  distrnq0  7458  prarloclem3  7496  genplt2i  7509  addlocpr  7535  prmuloc  7565  distrlem1prl  7581  distrlem1pru  7582  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  ltaprg  7618  prplnqu  7619  addextpr  7620  recexprlemdisj  7629  recexprlemloc  7630  aptiprleml  7638  aptiprlemu  7639  ltmprr  7641  archpr  7642  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  caucvgprlemnkj  7665  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemdisj  7701  caucvgprprlemloc  7702  caucvgprprlemaddq  7707  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  recexgt0sr  7772  mulgt0sr  7777  prsrriota  7787  suplocsrlem  7807  addcnsr  7833  mulcnsr  7834  mulcnsrec  7842  axmulcom  7870  rereceu  7888  axarch  7890  axcaucvglemres  7898  axpre-suploclemres  7900  lelttr  8046  ltletr  8047  addcan  8137  addcan2  8138  addsub4  8200  ltadd2  8376  le2add  8401  lt2add  8402  lt2sub  8417  le2sub  8418  eqord1  8440  rereim  8543  apreap  8544  apreim  8560  mulreim  8561  apcotr  8564  apadd1  8565  addext  8567  apneg  8568  mulext1  8569  mulext  8571  ltleap  8589  aprcl  8603  mulap0  8611  mulcanapd  8618  recapb  8628  rec11ap  8667  rec11rap  8668  divdivdivap  8670  ddcanap  8683  divadddivap  8684  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  lemulge11  8823  lt2mul2div  8836  ltrec  8840  lerec  8841  lerec2  8846  ledivp1  8860  mulle0r  8901  nn0ge0div  9340  suprzclex  9351  qapne  9639  xrlelttr  9806  xrltletr  9807  xrre3  9822  xrrege0  9825  xaddge0  9878  xle2add  9879  xlt2add  9880  fzass4  10062  fzrev  10084  elfz1b  10090  eluzgtdifelfzo  10197  fzocatel  10199  exbtwnzlemex  10250  rebtwn2z  10255  modqid  10349  modqcyc  10359  modqaddabs  10362  modqaddmod  10363  mulqaddmodid  10364  modqadd2mod  10374  modqltm1p1mod  10376  modqsubmod  10382  modqsubmodmod  10383  modaddmodup  10387  modqmulmod  10389  modqmulmodr  10390  modqaddmulmod  10391  modqsubdir  10393  frec2uzisod  10407  uzennn  10436  iseqovex  10456  seqvalcd  10459  seqf  10461  seqovcd  10463  seq3shft2  10473  monoord  10476  iseqf1olemnab  10488  seq3distr  10513  expnegzap  10554  ltexp2a  10572  le2sq2  10596  bernneq  10641  expnlbnd2  10646  nn0ltexp2  10689  nn0opth2  10704  faclbnd  10721  bcval5  10743  hashcl  10761  hashen  10764  fihashdom  10783  hashunlem  10784  hashun  10785  hashxp  10806  fimaxq  10807  zfz1isolem1  10820  zfz1iso  10821  seq3coll  10822  cvg1nlemres  10994  cvg1n  10995  resqrexlemp1rp  11015  resqrexlemoverl  11030  resqrexlemex  11034  sqrtsq  11053  abslt  11097  absle  11098  abs3lem  11120  maxleastlt  11224  maxltsup  11227  fimaxre2  11235  negfi  11236  xrmaxleastlt  11264  xrmaxltsup  11266  xrmaxaddlem  11268  2clim  11309  climcn2  11317  addcn2  11318  mulcn2  11320  reccn2ap  11321  climge0  11333  climcau  11355  summodclem2  11390  summodc  11391  zsumdc  11392  fsumf1o  11398  fisumss  11400  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  mptfzshft  11450  fsumrev  11451  fsummulc2  11456  fsumconst  11462  modfsummod  11466  fsumrelem  11479  binom  11492  cvgratnn  11539  mertenslemub  11542  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodf1o  11596  fprodssdc  11598  fprodmul  11599  fprodcl2lem  11613  fprodrev  11627  fprodconst  11628  fprodap0  11629  fprodrec  11637  fprodap0f  11644  fprodle  11648  fprodmodd  11649  efcllem  11667  tanaddaplem  11746  moddvds  11806  dvdsflip  11857  oexpneg  11882  nn0o  11912  fldivndvdslt  11940  zsupcllemstep  11946  zsupcllemex  11947  zssinfcl  11949  suprzubdc  11953  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemeu  12008  dfgcd3  12011  dfgcd2  12015  dvdsmulgcd  12026  bezoutr  12033  lcmgcdlem  12077  coprmdvds2  12093  qredeu  12097  rpdvds  12099  cncongr1  12103  prmind2  12120  isprm5lem  12141  isprm6  12147  oddpwdclemdc  12173  nonsq  12207  hashdvds  12221  crth  12224  eulerthlemh  12231  prmdiveq  12236  hashgcdlem  12238  hashgcdeq  12239  nnnn0modprm0  12255  pclemub  12287  pceu  12295  pcmul  12301  pcqmul  12303  pcgcd1  12327  pc2dvds  12329  difsqpwdvds  12337  pcmpt  12341  prmpwdvds  12353  1arith  12365  mul4sq  12392  ennnfonelemg  12404  ennnfonelemex  12415  ennnfonelemrnh  12417  ennnfonelemf1  12419  ennnfonelemrn  12420  ennnfonelemdm  12421  ennnfonelemim  12425  ennnfone  12426  ctinf  12431  ctiunctlemfo  12440  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  unbendc  12455  isstruct2r  12473  setscom  12502  ercpbl  12750  opifismgmdc  12790  grprinvlem  12804  mndpropd  12841  issubmnd  12843  submnd0  12845  mhmf1o  12861  0mhm  12873  mhmco  12874  mhmima  12875  mhmeql  12876  grprcan  12910  grpinvid1  12924  grpinvid2  12925  grplcan  12932  grplmulf1o  12944  grpnpncan0  12966  dfgrp3mlem  12968  grplactcnv  12972  mulgval  12986  mulgfng  12987  mulg1  12990  mulgnnp1  12991  mulgneg  13001  mulgnndir  13012  mulgdirlem  13014  mulgnn0ass  13019  mulgass  13020  subgmulg  13048  issubg4m  13053  subsubg  13057  subgintm  13058  isnsg3  13067  eqgcpbl  13087  ablpncan3  13120  srglmhm  13176  srgrmhm  13177  ringpropd  13217  dvdsrvald  13262  dvdsrd  13263  dvdsrex  13267  dvdsrtr  13270  unitpropdg  13317  subrgintm  13364  subsubrg  13366  aprap  13376  lmodprop2d  13438  rmodislmod  13441  iuncld  13618  ssnei2  13660  topssnei  13665  restopnb  13684  cnfval  13697  cnpfval  13698  iscnp4  13721  cnptopco  13725  cncnpi  13731  cncnp  13733  cnconst2  13736  cnrest2  13739  cnptoprest  13742  cnptoprest2  13743  cnpdis  13745  lmss  13749  lmtopcnp  13753  neitx  13771  txcnp  13774  txrest  13779  txdis1cn  13781  txlm  13782  cnmpt21  13794  imasnopn  13802  xmetres2  13882  blvalps  13891  blval  13892  elbl2ps  13895  elbl2  13896  blhalf  13911  blssexps  13932  blssex  13933  ssblex  13934  blin2  13935  bdmetval  14003  xmetxp  14010  xmettx  14013  metcnpi3  14020  txmetcnp  14021  addcncntoplem  14054  fsumcncntop  14059  elcncf2  14064  mulc1cncf  14079  cncfco  14081  cncfmet  14082  cncfmptc  14085  mulcncf  14094  dedekindeulemub  14099  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeu  14104  dedekindicclemub  14108  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimo  14137  cnplimccntop  14142  limccnp2lem  14148  limccnp2cntop  14149  dvfvalap  14153  dveflem  14190  reeff1olem  14195  reeff1oleme  14196  eflt  14199  sin0pilem2  14206  pilem3  14207  ioocosf1o  14278  cxplt  14339  cxple  14340  cxplt3  14343  apcxp2  14361  rprelogbmul  14376  rprelogbdiv  14378  logbgt0b  14387  logbgcd1irrap  14391  lgsdir2lem5  14436  lgsdi  14441  lgsne0  14442  lgseisenlem2  14454  2sqlem6  14470  2sqlem8  14473  2sqlem9  14474  2sqlem10  14475  nnti  14747  pwtrufal  14750  pwf1oexmid  14752  sssneq  14754  qdencn  14778  cvgcmp2n  14784  trilpolemlt1  14792  trirec0  14795  redc0  14808  reap0  14809  nconstwlpolemgt0  14814  neap0mkv  14819  supfz  14821  inffz  14822