Theorem simprr 498

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  simp1rr  1004  simp2rr  1008  simp3rr  1012  reg2exmidlema  4277  reg3exmidlemwe  4321  fvmptt  5283  fcof1  5443  fliftfun  5456  isotr  5476  riotass2  5514  acexmidlemab  5526  ovmpt2df  5652  grprinvlem  5715  1stconst  5862  2ndconst  5863  cnvf1olem  5865  f1od2  5876  smoiso  5940  swoer  6157  erinxp  6203  ecopovsymg  6228  th3qlem1  6231  f1imaen2g  6296  fidifsnen  6355  fiunsnnn  6365  fisbth  6367  findcard2d  6375  findcard2sd  6376  diffifi  6378  ac6sfi  6379  nnwetri  6382  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  supmaxti  6417  infminti  6440  ordiso2  6446  dfplpq2  6544  dfmpq2  6545  mulpipqqs  6563  distrnqg  6577  enq0sym  6622  enq0tr  6624  distrnq0  6649  prarloclem3  6687  genplt2i  6700  addlocpr  6726  prmuloc  6756  distrlem1prl  6772  distrlem1pru  6773  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltaprg  6809  prplnqu  6810  addextpr  6811  recexprlemdisj  6820  recexprlemloc  6821  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  archpr  6833  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  caucvgprlemnkj  6856  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  caucvgprprlemaddq  6898  recexgt0sr  6950  mulgt0sr  6954  prsrriota  6964  addcnsr  7002  mulcnsr  7003  mulcnsrec  7011  axmulcom  7037  rereceu  7055  axarch  7057  axcaucvglemres  7065  lelttr  7199  ltletr  7200  addcan  7288  addcan2  7289  addsub4  7351  ltadd2  7523  le2add  7548  lt2add  7549  lt2sub  7564  le2sub  7565  rereim  7686  apreap  7687  apreim  7703  mulreim  7704  apcotr  7707  apadd1  7708  addext  7710  apneg  7711  mulext1  7712  mulext  7714  ltleap  7730  mulap0  7744  mulcanapd  7751  rec11ap  7798  rec11rap  7799  divdivdivap  7801  ddcanap  7814  divadddivap  7815  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  lemulge11  7944  lt2mul2div  7957  ltrec  7961  lerec  7962  lerec2  7967  ledivp1  7981  mulle0r  8022  nn0ge0div  8434  suprzclex  8445  qapne  8724  xrlelttr  8876  xrltletr  8877  xrre3  8889  xrrege0  8892  fzass4  9080  fzrev  9101  elfz1b  9107  eluzgtdifelfzo  9206  fzocatel  9208  qbtwnzlemex  9259  rebtwn2z  9263  modqid  9351  modqcyc  9361  modqaddabs  9364  modqaddmod  9365  mulqaddmodid  9366  modqadd2mod  9376  modqltm1p1mod  9378  modqsubmod  9384  modqsubmodmod  9385  modaddmodup  9389  modqmulmod  9391  modqmulmodr  9392  modqaddmulmod  9393  modqsubdir  9395  frec2uzisod  9409  iseqovex  9439  iseqval  9440  iseqshft2  9452  monoord  9455  iseqdistr  9470  expnegzap  9510  ltexp2a  9528  le2sq2  9551  bernneq  9593  expnlbnd2  9598  nn0opth2  9651  faclbnd  9668  ibcval5  9690  cvg1nlemres  9871  cvg1n  9872  resqrexlemp1rp  9892  resqrexlemoverl  9907  resqrexlemex  9911  sqrtsq  9930  abslt  9974  absle  9975  abs3lem  9997  maxleastlt  10101  maxltsup  10104  fimaxre2  10109  negfi  10110  2clim  10140  climcn2  10148  addcn2  10149  mulcn2  10151  climge0  10163  climcau  10184  moddvds  10204  dvdsflip  10251  oexpneg  10276  nn0o  10307  fldivndvdslt  10335  zsupcllemstep  10341  zsupcllemex  10342  zssinfcl  10344  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemeu  10396  dfgcd3  10399  dfgcd2  10403  dvdsmulgcd  10414  bezoutr  10421  lcmgcdlem  10459  coprmdvds2  10475  qredeu  10479  rpdvds  10481  cncongr1  10485  prmind2  10502  isprm6  10526  oddpwdclemdc  10551  qdencn  10785