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  6423  tfrlem1  6538  tfr1onlemaccex  6578  tfrcllemaccex  6591  frecabcl  6629  fopwdom  7088  phplem4dom  7115  phpm  7119  phplem4on  7121  fidifsnen  7124  diffisn  7149  diffifi  7150  en2eqpr  7166  fisseneq  7194  suplub2ti  7291  difinfsn  7390  ctmlemr  7398  ctm  7399  ctssdclemn0  7400  ctssdc  7403  nninfninc  7413  nninfisol  7423  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  nninfwlpoimlemginf  7466  exmidontriimlem4  7530  exmidontriim  7531  cc3  7578  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  ltexnqq  7719  enq0tr  7745  addcmpblnq0  7754  mulcmpblnq0  7755  nnnq0lem1  7757  prssnqu  7791  prarloclemup  7806  nqprl  7862  nqpru  7863  mullocpr  7882  cauappcvgprlemladdfu  7965  cauappcvgprlemladdrl  7968  caucvgprlemm  7979  caucvgprlemladdfu  7988  caucvgprlemladdrl  7989  caucvgprlemlim  7992  caucvgprprlemml  8005  caucvgprprlemloc  8014  caucvgprprlemlim  8022  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemdisj  8031  suplocexprlemloc  8032  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  ltsrprg  8058  srpospr  8094  caucvgsrlemoffres  8111  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  axcaucvglemcau  8209  axsuploc  8342  cnegexlem3  8446  negeu  8460  add20  8744  rimul  8855  apreap  8857  cru  8872  apreim  8873  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  apti  8892  aptap  8920  mulap0  8924  prodgt0  9122  ltmul12a  9130  ledivdiv  9160  lediv12a  9164  supinfneg  9923  infsupneg  9924  qapne  9967  xaddf  10173  xaddval  10174  xleadd1a  10202  xleaddadd  10216  ixxss12  10235  ioodisj  10322  fznlem  10371  zsupcllemstep  10585  qtri3or  10596  exbtwnzlemstep  10603  rebtwn2zlemstep  10608  addmodlteq  10756  seqf1og  10879  mulexpzap  10937  leexp1a  10952  expnbnd  11021  apexp1  11076  faclbnd  11099  hashxp  11186  sshashneg  11198  zfz1iso  11206  swrdswrdlem  11389  cjap  11584  caucvgre  11659  cvg1nlemres  11663  resqrexlemglsq  11700  resqrexlemga  11701  sqrtsq  11722  ltabs  11765  abs3lem  11789  cau3lem  11792  maxleim  11883  rexico  11899  minmax  11908  xrmaxleim  11922  xrmaxiflemcl  11923  xrmaxiflemlub  11926  xrmaxiflemval  11928  xrmaxltsup  11936  xrmaxadd  11939  xrminmax  11943  xrbdtri  11954  climcau  12025  climrecvg1n  12026  sumeq2  12037  summodclem2  12061  divcnv  12176  prodeq2  12236  fprodsplitdc  12275  fprodconst  12299  dvdsle  12523  bitsfzo  12634  dvdsbnd  12645  bezoutlemmain  12687  bezoutlemzz  12691  bezoutlembi  12694  dfgcd3  12699  dvdsmulgcd  12714  nnmindc  12723  lcmcllem  12757  lcmgcdlem  12767  ncoprmgcdne1b  12779  isprm5  12832  pw2dvdslemn  12855  oddpwdclemxy  12859  pythagtriplem2  12957  pythagtrip  12974  pceu  12986  pc2dvds  13021  pcz  13023  pcadd  13031  pcfac  13041  exmidunben  13166  ctiunctlemfo  13179  unct  13182  prdsval  13475  sgrppropd  13615  sgrpidmndm  13622  mndpropd  13642  mhmeql  13694  isgrpinv  13756  dfgrp3mlem  13800  mhmmnd  13822  conjnmzb  13986  ghmcmn  14033  gsumfzconst  14047  isrng  14067  issrg  14098  isring  14133  dvdsrmul1  14236  tgrest  15021  cnpnei  15071  cnss1  15078  cncnp  15082  ismet2  15206  metequiv2  15348  metcnp  15364  metcnp2  15365  metcnpi3  15369  fsumcncntop  15419  elcncf2  15426  cncfmet  15444  suplociccreex  15476  dedekindicclemicc  15484  ivthinclemlr  15489  ivthinclemur  15491  cnplimclemr  15521  limccnpcntop  15527  limccoap  15530  dvmptfsum  15577  elply2  15587  plyrecj  15615  mersenne  15852  lgsval2lem  15870  lgsquad3  15944  usgr1eop  16227  usgr1vr  16230  pw1ndom3  16751  nninfalllem1  16773  nnnninfex  16787  sbthom  16793  apdiff  16819