Theorem simprr 499

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 475	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  1007  simp2rr  1011  simp3rr  1015  reg2exmidlema  4323  reg3exmidlemwe  4367  fvmptt  5357  fcof1  5523  fliftfun  5536  isotr  5556  riotass2  5595  acexmidlemab  5607  ovmpt2df  5733  grprinvlem  5796  1stconst  5943  2ndconst  5944  cnvf1olem  5946  f1od2  5957  smoiso  6021  tfrcldm  6082  tfrcl  6083  swoer  6272  erinxp  6318  ecopovsymg  6343  th3qlem1  6346  f1imaen2g  6462  mapdom1g  6515  fict  6536  fidifsnen  6538  dif1enen  6548  fiunsnnn  6549  fisbth  6551  findcard2d  6559  findcard2sd  6560  diffifi  6562  ac6sfi  6566  fimax2gtri  6569  nnwetri  6578  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  fisseneq  6592  ssfirab  6593  sbthlemi6  6615  sbthlemi8  6617  isbth  6620  supmaxti  6643  infminti  6666  ordiso2  6672  eldju2ndl  6707  eldju2ndr  6708  fodjuomnilemm  6745  fodjuomnilem0  6746  exmidfodomrlemrALT  6773  dfplpq2  6857  dfmpq2  6858  mulpipqqs  6876  distrnqg  6890  enq0sym  6935  enq0tr  6937  distrnq0  6962  prarloclem3  7000  genplt2i  7013  addlocpr  7039  prmuloc  7069  distrlem1prl  7085  distrlem1pru  7086  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  ltaprg  7122  prplnqu  7123  addextpr  7124  recexprlemdisj  7133  recexprlemloc  7134  aptiprleml  7142  aptiprlemu  7143  ltmprr  7145  archpr  7146  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlem1  7162  cauappcvgprlemlim  7164  caucvgprlemnkj  7169  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  caucvgprprlemaddq  7211  recexgt0sr  7263  mulgt0sr  7267  prsrriota  7277  addcnsr  7315  mulcnsr  7316  mulcnsrec  7324  axmulcom  7350  rereceu  7368  axarch  7370  axcaucvglemres  7378  lelttr  7517  ltletr  7518  addcan  7606  addcan2  7607  addsub4  7669  ltadd2  7841  le2add  7866  lt2add  7867  lt2sub  7882  le2sub  7883  rereim  8004  apreap  8005  apreim  8021  mulreim  8022  apcotr  8025  apadd1  8026  addext  8028  apneg  8029  mulext1  8030  mulext  8032  ltleap  8048  mulap0  8062  mulcanapd  8069  rec11ap  8116  rec11rap  8117  divdivdivap  8119  ddcanap  8132  divadddivap  8133  prodgt0gt0  8247  prodgt0  8248  prodge0  8250  lemulge11  8262  lt2mul2div  8275  ltrec  8279  lerec  8280  lerec2  8285  ledivp1  8299  mulle0r  8340  nn0ge0div  8766  suprzclex  8777  qapne  9056  xrlelttr  9203  xrltletr  9204  xrre3  9216  xrrege0  9219  fzass4  9407  fzrev  9428  elfz1b  9434  eluzgtdifelfzo  9536  fzocatel  9538  exbtwnzlemex  9589  rebtwn2z  9594  modqid  9684  modqcyc  9694  modqaddabs  9697  modqaddmod  9698  mulqaddmodid  9699  modqadd2mod  9709  modqltm1p1mod  9711  modqsubmod  9717  modqsubmodmod  9718  modaddmodup  9722  modqmulmod  9724  modqmulmodr  9725  modqaddmulmod  9726  modqsubdir  9728  frec2uzisod  9742  iseqovex  9787  iseqval  9788  iseqfclt  9794  iseqshft2  9806  monoord  9809  iseqf1olemnab  9821  iseqdistr  9846  expnegzap  9887  ltexp2a  9905  le2sq2  9928  bernneq  9970  expnlbnd2  9975  nn0opth2  10028  faclbnd  10045  ibcval5  10067  hashcl  10085  hashen  10088  fihashdom  10107  hashunlem  10108  hashun  10109  hashxp  10130  fimaxq  10131  zfz1isolem1  10141  zfz1iso  10142  iseqcoll  10143  cvg1nlemres  10313  cvg1n  10314  resqrexlemp1rp  10334  resqrexlemoverl  10349  resqrexlemex  10353  sqrtsq  10372  abslt  10416  absle  10417  abs3lem  10439  maxleastlt  10543  maxltsup  10546  fimaxre2  10551  negfi  10552  2clim  10582  climcn2  10590  addcn2  10591  mulcn2  10593  climge0  10605  climcau  10626  isummolem2  10661  isummo  10662  zisum  10663  fsumf1o  10668  fisumss  10670  moddvds  10680  dvdsflip  10727  oexpneg  10752  nn0o  10782  fldivndvdslt  10810  zsupcllemstep  10816  zsupcllemex  10817  zssinfcl  10819  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlemeu  10871  dfgcd3  10874  dfgcd2  10878  dvdsmulgcd  10889  bezoutr  10896  lcmgcdlem  10934  coprmdvds2  10950  qredeu  10954  rpdvds  10956  cncongr1  10960  prmind2  10977  isprm6  11001  oddpwdclemdc  11026  nonsq  11060  hashdvds  11072  crth  11075  hashgcdlem  11078  hashgcdeq  11079  nnsucpred  11329  nnti  11330  qdencn  11353