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  6281  tfrlem1  6361  tfr1onlemaccex  6401  tfrcllemaccex  6414  frecabcl  6452  fopwdom  6892  phplem4dom  6918  phpm  6921  phplem4on  6923  fidifsnen  6926  diffisn  6949  diffifi  6950  en2eqpr  6963  fisseneq  6988  suplub2ti  7060  difinfsn  7159  ctmlemr  7167  ctm  7168  ctssdclemn0  7169  ctssdc  7172  nninfninc  7182  nninfisol  7192  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  nninfwlpoimlemginf  7235  exmidontriimlem4  7284  exmidontriim  7285  cc3  7328  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  ltexnqq  7468  enq0tr  7494  addcmpblnq0  7503  mulcmpblnq0  7504  nnnq0lem1  7506  prssnqu  7540  prarloclemup  7555  nqprl  7611  nqpru  7612  mullocpr  7631  cauappcvgprlemladdfu  7714  cauappcvgprlemladdrl  7717  caucvgprlemm  7728  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlemlim  7741  caucvgprprlemml  7754  caucvgprprlemloc  7763  caucvgprprlemlim  7771  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  ltsrprg  7807  srpospr  7843  caucvgsrlemoffres  7860  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axcaucvglemcau  7958  axsuploc  8092  cnegexlem3  8196  negeu  8210  add20  8493  rimul  8604  apreap  8606  cru  8621  apreim  8622  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  apti  8641  aptap  8669  mulap0  8673  prodgt0  8871  ltmul12a  8879  ledivdiv  8909  lediv12a  8913  supinfneg  9660  infsupneg  9661  qapne  9704  xaddf  9910  xaddval  9911  xleadd1a  9939  xleaddadd  9953  ixxss12  9972  ioodisj  10059  fznlem  10107  qtri3or  10310  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  addmodlteq  10469  seqf1og  10592  mulexpzap  10650  leexp1a  10665  expnbnd  10734  apexp1  10789  faclbnd  10812  hashxp  10897  zfz1iso  10912  cjap  11050  caucvgre  11125  cvg1nlemres  11129  resqrexlemglsq  11166  resqrexlemga  11167  sqrtsq  11188  ltabs  11231  abs3lem  11255  cau3lem  11258  maxleim  11349  rexico  11365  minmax  11373  xrmaxleim  11387  xrmaxiflemcl  11388  xrmaxiflemlub  11391  xrmaxiflemval  11393  xrmaxltsup  11401  xrmaxadd  11404  xrminmax  11408  xrbdtri  11419  climcau  11490  climrecvg1n  11491  sumeq2  11502  summodclem2  11525  divcnv  11640  prodeq2  11700  fprodsplitdc  11739  fprodconst  11763  dvdsle  11986  zsupcllemstep  12082  dvdsbnd  12093  bezoutlemmain  12135  bezoutlemzz  12139  bezoutlembi  12142  dfgcd3  12147  dvdsmulgcd  12162  nnmindc  12171  lcmcllem  12205  lcmgcdlem  12215  ncoprmgcdne1b  12227  isprm5  12280  pw2dvdslemn  12303  oddpwdclemxy  12307  pythagtriplem2  12404  pythagtrip  12421  pceu  12433  pc2dvds  12468  pcz  12470  pcadd  12478  pcfac  12488  exmidunben  12583  ctiunctlemfo  12596  unct  12599  sgrppropd  12996  sgrpidmndm  13001  mndpropd  13021  mhmeql  13064  isgrpinv  13126  dfgrp3mlem  13170  mhmmnd  13186  conjnmzb  13350  ghmcmn  13397  gsumfzconst  13411  isrng  13430  issrg  13461  isring  13496  reldvdsrsrg  13588  dvdsrmul1  13598  tgrest  14337  cnpnei  14387  cnss1  14394  cncnp  14398  ismet2  14522  metequiv2  14664  metcnp  14680  metcnp2  14681  metcnpi3  14685  fsumcncntop  14724  elcncf2  14729  cncfmet  14747  suplociccreex  14778  dedekindicclemicc  14786  ivthinclemlr  14791  ivthinclemur  14793  cnplimclemr  14823  limccnpcntop  14829  limccoap  14832  elply2  14881  lgsval2lem  15126  nninfalllem1  15498  sbthom  15516  apdiff  15538