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  6393  tfrlem1  6474  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecabcl  6565  fopwdom  7022  phplem4dom  7048  phpm  7052  phplem4on  7054  fidifsnen  7057  diffisn  7082  diffifi  7083  en2eqpr  7099  fisseneq  7127  suplub2ti  7200  difinfsn  7299  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdc  7312  nninfninc  7322  nninfisol  7332  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemginf  7375  exmidontriimlem4  7439  exmidontriim  7440  cc3  7487  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prssnqu  7700  prarloclemup  7715  nqprl  7771  nqpru  7772  mullocpr  7791  cauappcvgprlemladdfu  7874  cauappcvgprlemladdrl  7877  caucvgprlemm  7888  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemloc  7923  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  srpospr  8003  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axsuploc  8252  cnegexlem3  8356  negeu  8370  add20  8654  rimul  8765  apreap  8767  cru  8782  apreim  8783  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  apti  8802  aptap  8830  mulap0  8834  prodgt0  9032  ltmul12a  9040  ledivdiv  9070  lediv12a  9074  supinfneg  9829  infsupneg  9830  qapne  9873  xaddf  10079  xaddval  10080  xleadd1a  10108  xleaddadd  10122  ixxss12  10141  ioodisj  10228  fznlem  10276  zsupcllemstep  10490  qtri3or  10501  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  addmodlteq  10661  seqf1og  10784  mulexpzap  10842  leexp1a  10857  expnbnd  10926  apexp1  10981  faclbnd  11004  hashxp  11091  zfz1iso  11106  swrdswrdlem  11286  cjap  11468  caucvgre  11543  cvg1nlemres  11547  resqrexlemglsq  11584  resqrexlemga  11585  sqrtsq  11606  ltabs  11649  abs3lem  11673  cau3lem  11676  maxleim  11767  rexico  11783  minmax  11792  xrmaxleim  11806  xrmaxiflemcl  11807  xrmaxiflemlub  11810  xrmaxiflemval  11812  xrmaxltsup  11820  xrmaxadd  11823  xrminmax  11827  xrbdtri  11838  climcau  11909  climrecvg1n  11910  sumeq2  11921  summodclem2  11945  divcnv  12060  prodeq2  12120  fprodsplitdc  12159  fprodconst  12183  dvdsle  12407  bitsfzo  12518  dvdsbnd  12529  bezoutlemmain  12571  bezoutlemzz  12575  bezoutlembi  12578  dfgcd3  12583  dvdsmulgcd  12598  nnmindc  12607  lcmcllem  12641  lcmgcdlem  12651  ncoprmgcdne1b  12663  isprm5  12716  pw2dvdslemn  12739  oddpwdclemxy  12743  pythagtriplem2  12841  pythagtrip  12858  pceu  12870  pc2dvds  12905  pcz  12907  pcadd  12915  pcfac  12925  exmidunben  13049  ctiunctlemfo  13062  unct  13065  prdsval  13358  sgrppropd  13498  sgrpidmndm  13505  mndpropd  13525  mhmeql  13577  isgrpinv  13639  dfgrp3mlem  13683  mhmmnd  13705  conjnmzb  13869  ghmcmn  13916  gsumfzconst  13930  isrng  13950  issrg  13981  isring  14016  dvdsrmul1  14119  tgrest  14896  cnpnei  14946  cnss1  14953  cncnp  14957  ismet2  15081  metequiv2  15223  metcnp  15239  metcnp2  15240  metcnpi3  15244  fsumcncntop  15294  elcncf2  15301  cncfmet  15319  suplociccreex  15351  dedekindicclemicc  15359  ivthinclemlr  15364  ivthinclemur  15366  cnplimclemr  15396  limccnpcntop  15402  limccoap  15405  dvmptfsum  15452  elply2  15462  plyrecj  15490  mersenne  15724  lgsval2lem  15742  lgsquad3  15816  usgr1eop  16099  usgr1vr  16102  pw1ndom3  16610  nninfalllem1  16631  nnnninfex  16645  sbthom  16651  apdiff  16673