Theorem simprr 521

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rr  1047  simp2rr  1051  simp3rr  1055  disjiun  3919  reg2exmidlema  4444  reg3exmidlemwe  4488  nnsucpred  4525  fvmptt  5505  fcof1  5677  fliftfun  5690  isotr  5710  riotass2  5749  acexmidlemab  5761  ovmpodf  5895  grprinvlem  5958  fnmpoovd  6105  1stconst  6111  2ndconst  6112  cnvf1olem  6114  f1od2  6125  smoiso  6192  tfrcldm  6253  tfrcl  6254  nntr2  6392  swoer  6450  erinxp  6496  ecopovsymg  6521  th3qlem1  6524  f1imaen2g  6680  mapdom1g  6734  fict  6755  fidifsnen  6757  dif1enen  6767  fiunsnnn  6768  fisbth  6770  findcard2d  6778  findcard2sd  6779  diffifi  6781  ac6sfi  6785  fimax2gtri  6788  nnwetri  6797  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  fisseneq  6813  ssfirab  6815  fidcenumlemrk  6835  fidcenumlemr  6836  sbthlemi6  6843  sbthlemi8  6845  isbth  6848  fiuni  6859  supmaxti  6884  infminti  6907  ordiso2  6913  eldju2ndl  6950  eldju2ndr  6951  omp1eomlem  6972  difinfsnlem  6977  difinfinf  6979  ctmlemr  6986  ctssdccl  6989  fodjum  7011  fodju0  7012  exmidfodomrlemrALT  7052  acfun  7056  exmidaclem  7057  ccfunen  7072  dfplpq2  7155  dfmpq2  7156  mulpipqqs  7174  distrnqg  7188  enq0sym  7233  enq0tr  7235  distrnq0  7260  prarloclem3  7298  genplt2i  7311  addlocpr  7337  prmuloc  7367  distrlem1prl  7383  distrlem1pru  7384  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  ltaprg  7420  prplnqu  7421  addextpr  7422  recexprlemdisj  7431  recexprlemloc  7432  aptiprleml  7440  aptiprlemu  7441  ltmprr  7443  archpr  7444  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlem1  7460  cauappcvgprlemlim  7462  caucvgprlemnkj  7467  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemnjltk  7492  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemdisj  7503  caucvgprprlemloc  7504  caucvgprprlemaddq  7509  suplocexprlemrl  7518  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemex  7523  suplocexprlemub  7524  recexgt0sr  7574  mulgt0sr  7579  prsrriota  7589  suplocsrlem  7609  addcnsr  7635  mulcnsr  7636  mulcnsrec  7644  axmulcom  7672  rereceu  7690  axarch  7692  axcaucvglemres  7700  axpre-suploclemres  7702  lelttr  7845  ltletr  7846  addcan  7935  addcan2  7936  addsub4  7998  ltadd2  8174  le2add  8199  lt2add  8200  lt2sub  8215  le2sub  8216  eqord1  8238  rereim  8341  apreap  8342  apreim  8358  mulreim  8359  apcotr  8362  apadd1  8363  addext  8365  apneg  8366  mulext1  8367  mulext  8369  ltleap  8387  aprcl  8401  mulap0  8408  mulcanapd  8415  rec11ap  8463  rec11rap  8464  divdivdivap  8466  ddcanap  8479  divadddivap  8480  prodgt0gt0  8602  prodgt0  8603  prodge0  8605  lemulge11  8617  lt2mul2div  8630  ltrec  8634  lerec  8635  lerec2  8640  ledivp1  8654  mulle0r  8695  nn0ge0div  9131  suprzclex  9142  qapne  9424  xrlelttr  9582  xrltletr  9583  xrre3  9598  xrrege0  9601  xaddge0  9654  xle2add  9655  xlt2add  9656  fzass4  9835  fzrev  9857  elfz1b  9863  eluzgtdifelfzo  9967  fzocatel  9969  exbtwnzlemex  10020  rebtwn2z  10025  modqid  10115  modqcyc  10125  modqaddabs  10128  modqaddmod  10129  mulqaddmodid  10130  modqadd2mod  10140  modqltm1p1mod  10142  modqsubmod  10148  modqsubmodmod  10149  modaddmodup  10153  modqmulmod  10155  modqmulmodr  10156  modqaddmulmod  10157  modqsubdir  10159  frec2uzisod  10173  uzennn  10202  iseqovex  10222  seqvalcd  10225  seqf  10227  seqovcd  10229  seq3shft2  10239  monoord  10242  iseqf1olemnab  10254  seq3distr  10279  expnegzap  10320  ltexp2a  10338  le2sq2  10361  bernneq  10405  expnlbnd2  10410  nn0opth2  10463  faclbnd  10480  bcval5  10502  hashcl  10520  hashen  10523  fihashdom  10542  hashunlem  10543  hashun  10544  hashxp  10565  fimaxq  10566  zfz1isolem1  10576  zfz1iso  10577  seq3coll  10578  cvg1nlemres  10750  cvg1n  10751  resqrexlemp1rp  10771  resqrexlemoverl  10786  resqrexlemex  10790  sqrtsq  10809  abslt  10853  absle  10854  abs3lem  10876  maxleastlt  10980  maxltsup  10983  fimaxre2  10991  negfi  10992  xrmaxleastlt  11018  xrmaxltsup  11020  xrmaxaddlem  11022  2clim  11063  climcn2  11071  addcn2  11072  mulcn2  11074  reccn2ap  11075  climge0  11087  climcau  11109  summodclem2  11144  summodc  11145  zsumdc  11146  fsumf1o  11152  fisumss  11154  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  mptfzshft  11204  fsumrev  11205  fsummulc2  11210  fsumconst  11216  modfsummod  11220  fsumrelem  11233  binom  11246  cvgratnn  11293  mertenslemub  11296  efcllem  11354  tanaddaplem  11434  moddvds  11491  dvdsflip  11538  oexpneg  11563  nn0o  11593  fldivndvdslt  11621  zsupcllemstep  11627  zsupcllemex  11628  zssinfcl  11630  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemeu  11684  dfgcd3  11687  dfgcd2  11691  dvdsmulgcd  11702  bezoutr  11709  lcmgcdlem  11747  coprmdvds2  11763  qredeu  11767  rpdvds  11769  cncongr1  11773  prmind2  11790  isprm6  11814  oddpwdclemdc  11840  nonsq  11874  hashdvds  11886  crth  11889  hashgcdlem  11892  hashgcdeq  11893  ennnfonelemg  11905  ennnfonelemex  11916  ennnfonelemrnh  11918  ennnfonelemf1  11920  ennnfonelemrn  11921  ennnfonelemdm  11922  ennnfonelemim  11926  ennnfone  11927  ctinf  11932  ctiunctlemfo  11941  isstruct2r  11959  setscom  11988  iuncld  12273  ssnei2  12315  topssnei  12320  restopnb  12339  cnfval  12352  cnpfval  12353  iscnp4  12376  cnptopco  12380  cncnpi  12386  cncnp  12388  cnconst2  12391  cnrest2  12394  cnptoprest  12397  cnptoprest2  12398  cnpdis  12400  lmss  12404  lmtopcnp  12408  neitx  12426  txcnp  12429  txrest  12434  txdis1cn  12436  txlm  12437  cnmpt21  12449  imasnopn  12457  xmetres2  12537  blvalps  12546  blval  12547  elbl2ps  12550  elbl2  12551  blhalf  12566  blssexps  12587  blssex  12588  ssblex  12589  blin2  12590  bdmetval  12658  xmetxp  12665  xmettx  12668  metcnpi3  12675  txmetcnp  12676  addcncntoplem  12709  fsumcncntop  12714  elcncf2  12719  mulc1cncf  12734  cncfco  12736  cncfmet  12737  cncfmptc  12740  mulcncf  12749  dedekindeulemub  12754  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeu  12759  dedekindicclemub  12763  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemicc  12768  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimo  12792  cnplimccntop  12797  limccnp2lem  12803  limccnp2cntop  12804  dvfvalap  12808  dveflem  12844  sin0pilem2  12852  pilem3  12853  nnti  13180  pwtrufal  13181  pwf1oexmid  13183  qdencn  13211  cvgcmp2n  13217  trilpolemlt1  13223  supfz  13226  inffz  13227