Theorem simpllr 534

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  542  f1o2ndf1  6219  tfrlem1  6299  tfr1onlemaccex  6339  tfrcllemaccex  6352  frecabcl  6390  fopwdom  6826  phplem4dom  6852  phpm  6855  phplem4on  6857  fidifsnen  6860  diffisn  6883  diffifi  6884  en2eqpr  6897  fisseneq  6921  suplub2ti  6990  difinfsn  7089  ctmlemr  7097  ctm  7098  ctssdclemn0  7099  ctssdc  7102  nninfisol  7121  enomnilem  7126  enmkvlem  7149  enwomnilem  7157  nninfwlpoimlemginf  7164  exmidontriimlem4  7213  exmidontriim  7214  cc3  7242  addcmpblnq  7341  mulcmpblnq  7342  ordpipqqs  7348  ltexnqq  7382  enq0tr  7408  addcmpblnq0  7417  mulcmpblnq0  7418  nnnq0lem1  7420  prssnqu  7454  prarloclemup  7469  nqprl  7525  nqpru  7526  mullocpr  7545  cauappcvgprlemladdfu  7628  cauappcvgprlemladdrl  7631  caucvgprlemm  7642  caucvgprlemladdfu  7651  caucvgprlemladdrl  7652  caucvgprlemlim  7655  caucvgprprlemml  7668  caucvgprprlemloc  7677  caucvgprprlemlim  7685  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  addcmpblnr  7713  mulcmpblnrlemg  7714  mulcmpblnr  7715  ltsrprg  7721  srpospr  7757  caucvgsrlemoffres  7774  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  axcaucvglemcau  7872  axsuploc  8004  cnegexlem3  8108  negeu  8122  add20  8405  rimul  8516  apreap  8518  cru  8533  apreim  8534  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  apti  8553  mulap0  8584  prodgt0  8782  ltmul12a  8790  ledivdiv  8820  lediv12a  8824  supinfneg  9568  infsupneg  9569  qapne  9612  xaddf  9815  xaddval  9816  xleadd1a  9844  xleaddadd  9858  ixxss12  9877  ioodisj  9964  fznlem  10011  qtri3or  10213  exbtwnzlemstep  10218  rebtwn2zlemstep  10223  addmodlteq  10368  mulexpzap  10530  leexp1a  10545  expnbnd  10613  apexp1  10666  faclbnd  10689  hashxp  10774  zfz1iso  10789  cjap  10883  caucvgre  10958  cvg1nlemres  10962  resqrexlemglsq  10999  resqrexlemga  11000  sqrtsq  11021  ltabs  11064  abs3lem  11088  cau3lem  11091  maxleim  11182  rexico  11198  minmax  11206  xrmaxleim  11220  xrmaxiflemcl  11221  xrmaxiflemlub  11224  xrmaxiflemval  11226  xrmaxltsup  11234  xrmaxadd  11237  xrminmax  11241  xrbdtri  11252  climcau  11323  climrecvg1n  11324  sumeq2  11335  summodclem2  11358  divcnv  11473  prodeq2  11533  fprodsplitdc  11572  fprodconst  11596  dvdsle  11817  zsupcllemstep  11913  dvdsbnd  11924  gcdsupex  11925  gcdsupcl  11926  bezoutlemmain  11966  bezoutlemzz  11970  bezoutlembi  11973  dfgcd3  11978  dvdsmulgcd  11993  nnmindc  12002  lcmcllem  12034  lcmgcdlem  12044  ncoprmgcdne1b  12056  isprm5  12109  pw2dvdslemn  12132  oddpwdclemxy  12136  pythagtriplem2  12233  pythagtrip  12250  pceu  12262  pc2dvds  12296  pcz  12298  pcadd  12306  pcfac  12315  exmidunben  12394  ctiunctlemfo  12407  unct  12410  sgrpidmndm  12687  mndpropd  12707  mhmeql  12738  isgrpinv  12788  dfgrp3mlem  12829  mhmmnd  12841  issrg  12945  isring  12980  tgrest  13240  cnpnei  13290  cnss1  13297  cncnp  13301  ismet2  13425  metequiv2  13567  metcnp  13583  metcnp2  13584  metcnpi3  13588  fsumcncntop  13627  elcncf2  13632  cncfmet  13650  suplociccreex  13673  dedekindicclemicc  13681  ivthinclemlr  13686  ivthinclemur  13688  cnplimclemr  13709  limccnpcntop  13715  limccoap  13718  lgsval2lem  13982  nninfalllem1  14318  sbthom  14335  apdiff  14357