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  7584  addcmpblnq  7684  mulcmpblnq  7685  ordpipqqs  7691  ltexnqq  7725  enq0tr  7751  addcmpblnq0  7760  mulcmpblnq0  7761  nnnq0lem1  7763  prssnqu  7797  prarloclemup  7812  nqprl  7868  nqpru  7869  mullocpr  7888  cauappcvgprlemladdfu  7971  cauappcvgprlemladdrl  7974  caucvgprlemm  7985  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlemlim  7998  caucvgprprlemml  8011  caucvgprprlemloc  8020  caucvgprprlemlim  8028  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  addcmpblnr  8056  mulcmpblnrlemg  8057  mulcmpblnr  8058  ltsrprg  8064  srpospr  8100  caucvgsrlemoffres  8117  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axcaucvglemcau  8215  axsuploc  8348  cnegexlem3  8452  negeu  8466  add20  8750  rimul  8861  apreap  8863  cru  8878  apreim  8879  apsym  8882  apcotr  8883  apadd1  8884  apneg  8887  mulext1  8888  apti  8898  aptap  8926  mulap0  8930  prodgt0  9128  ltmul12a  9136  ledivdiv  9166  lediv12a  9170  supinfneg  9930  infsupneg  9931  qapne  9974  xaddf  10180  xaddval  10181  xleadd1a  10209  xleaddadd  10223  ixxss12  10242  ioodisj  10329  fznlem  10378  zsupcllemstep  10593  qtri3or  10604  exbtwnzlemstep  10611  rebtwn2zlemstep  10616  addmodlteq  10764  seqf1og  10887  mulexpzap  10945  leexp1a  10960  expnbnd  11029  apexp1  11084  faclbnd  11107  hashxp  11195  sshashneg  11209  zfz1iso  11217  swrdswrdlem  11400  cjap  11595  caucvgre  11670  cvg1nlemres  11674  resqrexlemglsq  11711  resqrexlemga  11712  sqrtsq  11733  ltabs  11776  abs3lem  11800  cau3lem  11803  maxleim  11894  rexico  11910  minmax  11919  xrmaxleim  11933  xrmaxiflemcl  11934  xrmaxiflemlub  11937  xrmaxiflemval  11939  xrmaxltsup  11947  xrmaxadd  11950  xrminmax  11954  xrbdtri  11965  climcau  12036  climrecvg1n  12037  sumeq2  12048  summodclem2  12072  divcnv  12187  prodeq2  12247  fprodsplitdc  12286  fprodconst  12310  dvdsle  12534  bitsfzo  12645  dvdsbnd  12656  bezoutlemmain  12698  bezoutlemzz  12702  bezoutlembi  12705  dfgcd3  12710  dvdsmulgcd  12725  nnmindc  12734  lcmcllem  12768  lcmgcdlem  12778  ncoprmgcdne1b  12790  isprm5  12843  pw2dvdslemn  12866  oddpwdclemxy  12870  pythagtriplem2  12968  pythagtrip  12985  pceu  12997  pc2dvds  13032  pcz  13034  pcadd  13042  pcfac  13052  exmidunben  13194  ctiunctlemfo  13207  unct  13210  prdsval  13503  sgrppropd  13643  sgrpidmndm  13650  mndpropd  13670  mhmeql  13722  isgrpinv  13784  dfgrp3mlem  13828  mhmmnd  13850  conjnmzb  14014  ghmcmn  14061  gsumfzconst  14075  isrng  14095  issrg  14126  isring  14161  dvdsrmul1  14264  aprlring  14451  tgrest  15051  cnpnei  15101  cnss1  15108  cncnp  15112  ismet2  15236  metequiv2  15378  metcnp  15394  metcnp2  15395  metcnpi3  15399  fsumcncntop  15449  elcncf2  15456  cncfmet  15474  suplociccreex  15506  dedekindicclemicc  15514  ivthinclemlr  15519  ivthinclemur  15521  cnplimclemr  15551  limccnpcntop  15557  limccoap  15560  dvmptfsum  15607  elply2  15617  plyrecj  15645  mersenne  15882  lgsval2lem  15900  lgsquad3  15974  usgr1eop  16257  usgr1vr  16260  pw1ndom3  16781  nninfalllem1  16803  nnnninfex  16817  sbthom  16823  apdiff  16849  trimul0or  16862