Theorem simpllr 536

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simpllr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 488	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:  simp-4r  544  f1o2ndf1  6426  tfrlem1  6541  tfr1onlemaccex  6581  tfrcllemaccex  6594  frecabcl  6632  fopwdom  7091  phplem4dom  7118  phpm  7122  phplem4on  7124  fidifsnen  7127  diffisn  7152  diffifi  7153  en2eqpr  7169  fisseneq  7197  suplub2ti  7294  difinfsn  7393  ctmlemr  7401  ctm  7402  ctssdclemn0  7403  ctssdc  7406  nninfninc  7416  nninfisol  7426  enomnilem  7431  enmkvlem  7454  enwomnilem  7462  nninfwlpoimlemginf  7469  exmidontriimlem4  7533  exmidontriim  7534  cc3  7587  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  ltexnqq  7728  enq0tr  7754  addcmpblnq0  7763  mulcmpblnq0  7764  nnnq0lem1  7766  prssnqu  7800  prarloclemup  7815  nqprl  7871  nqpru  7872  mullocpr  7891  cauappcvgprlemladdfu  7974  cauappcvgprlemladdrl  7977  caucvgprlemm  7988  caucvgprlemladdfu  7997  caucvgprlemladdrl  7998  caucvgprlemlim  8001  caucvgprprlemml  8014  caucvgprprlemloc  8023  caucvgprprlemlim  8031  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemdisj  8040  suplocexprlemloc  8041  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  ltsrprg  8067  srpospr  8103  caucvgsrlemoffres  8120  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  axcaucvglemcau  8218  axsuploc  8351  cnegexlem3  8455  negeu  8469  add20  8753  rimul  8864  apreap  8866  cru  8881  apreim  8882  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  apti  8901  aptap  8929  mulap0  8933  prodgt0  9131  ltmul12a  9139  ledivdiv  9169  lediv12a  9173  supinfneg  9933  infsupneg  9934  qapne  9977  xaddf  10183  xaddval  10184  xleadd1a  10212  xleaddadd  10226  ixxss12  10245  ioodisj  10332  fznlem  10381  zsupcllemstep  10596  qtri3or  10607  exbtwnzlemstep  10614  rebtwn2zlemstep  10619  addmodlteq  10767  seqf1og  10890  mulexpzap  10948  leexp1a  10963  expnbnd  11033  apexp1  11088  faclbnd  11111  hashxp  11199  sshashneg  11213  zfz1iso  11221  swrdswrdlem  11404  cjap  11599  caucvgre  11674  cvg1nlemres  11678  resqrexlemglsq  11715  resqrexlemga  11716  sqrtsq  11737  ltabs  11780  abs3lem  11804  cau3lem  11807  maxleim  11898  rexico  11914  minmax  11923  xrmaxleim  11937  xrmaxiflemcl  11938  xrmaxiflemlub  11941  xrmaxiflemval  11943  xrmaxltsup  11951  xrmaxadd  11954  xrminmax  11958  xrbdtri  11969  climcau  12040  climrecvg1n  12041  sumeq2  12052  summodclem2  12076  divcnv  12191  prodeq2  12251  fprodsplitdc  12290  fprodconst  12314  dvdsle  12538  bitsfzo  12649  dvdsbnd  12660  bezoutlemmain  12702  bezoutlemzz  12706  bezoutlembi  12709  dfgcd3  12714  dvdsmulgcd  12729  nnmindc  12738  lcmcllem  12772  lcmgcdlem  12782  ncoprmgcdne1b  12794  isprm5  12847  pw2dvdslemn  12870  oddpwdclemxy  12874  pythagtriplem2  12972  pythagtrip  12989  pceu  13001  pc2dvds  13036  pcz  13038  pcadd  13046  pcfac  13056  exmidunben  13198  ctiunctlemfo  13211  unct  13214  prdsval  13507  sgrppropd  13647  sgrpidmndm  13654  mndpropd  13674  mhmeql  13726  isgrpinv  13788  dfgrp3mlem  13832  mhmmnd  13854  conjnmzb  14018  ghmcmn  14065  gsumfzconst  14079  isrng  14099  issrg  14130  isring  14165  dvdsrmul1  14269  aprlring  14460  tgrest  15083  cnpnei  15133  cnss1  15140  cncnp  15144  ismet2  15268  metequiv2  15410  metcnp  15426  metcnp2  15427  metcnpi3  15431  fsumcncntop  15481  elcncf2  15488  cncfmet  15506  suplociccreex  15538  dedekindicclemicc  15546  ivthinclemlr  15551  ivthinclemur  15553  cnplimclemr  15583  limccnpcntop  15589  limccoap  15592  dvmptfsum  15639  elply2  15649  plyrecj  15677  mersenne  15914  lgsval2lem  15932  lgsquad3  16006  usgr1eop  16289  usgr1vr  16292  pw1ndom3  16813  nninfalllem1  16835  nnnninfex  16849  sbthom  16855  apdiff  16881  trimul0or  16894