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  6224  tfrlem1  6304  tfr1onlemaccex  6344  tfrcllemaccex  6357  frecabcl  6395  fopwdom  6831  phplem4dom  6857  phpm  6860  phplem4on  6862  fidifsnen  6865  diffisn  6888  diffifi  6889  en2eqpr  6902  fisseneq  6926  suplub2ti  6995  difinfsn  7094  ctmlemr  7102  ctm  7103  ctssdclemn0  7104  ctssdc  7107  nninfisol  7126  enomnilem  7131  enmkvlem  7154  enwomnilem  7162  nninfwlpoimlemginf  7169  exmidontriimlem4  7218  exmidontriim  7219  cc3  7262  addcmpblnq  7361  mulcmpblnq  7362  ordpipqqs  7368  ltexnqq  7402  enq0tr  7428  addcmpblnq0  7437  mulcmpblnq0  7438  nnnq0lem1  7440  prssnqu  7474  prarloclemup  7489  nqprl  7545  nqpru  7546  mullocpr  7565  cauappcvgprlemladdfu  7648  cauappcvgprlemladdrl  7651  caucvgprlemm  7662  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlemlim  7675  caucvgprprlemml  7688  caucvgprprlemloc  7697  caucvgprprlemlim  7705  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemloc  7715  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  ltsrprg  7741  srpospr  7777  caucvgsrlemoffres  7794  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  axcaucvglemcau  7892  axsuploc  8024  cnegexlem3  8128  negeu  8142  add20  8425  rimul  8536  apreap  8538  cru  8553  apreim  8554  apsym  8557  apcotr  8558  apadd1  8559  apneg  8562  mulext1  8563  apti  8573  aptap  8601  mulap0  8605  prodgt0  8803  ltmul12a  8811  ledivdiv  8841  lediv12a  8845  supinfneg  9589  infsupneg  9590  qapne  9633  xaddf  9838  xaddval  9839  xleadd1a  9867  xleaddadd  9881  ixxss12  9900  ioodisj  9987  fznlem  10034  qtri3or  10236  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  addmodlteq  10391  mulexpzap  10553  leexp1a  10568  expnbnd  10636  apexp1  10689  faclbnd  10712  hashxp  10797  zfz1iso  10812  cjap  10906  caucvgre  10981  cvg1nlemres  10985  resqrexlemglsq  11022  resqrexlemga  11023  sqrtsq  11044  ltabs  11087  abs3lem  11111  cau3lem  11114  maxleim  11205  rexico  11221  minmax  11229  xrmaxleim  11243  xrmaxiflemcl  11244  xrmaxiflemlub  11247  xrmaxiflemval  11249  xrmaxltsup  11257  xrmaxadd  11260  xrminmax  11264  xrbdtri  11275  climcau  11346  climrecvg1n  11347  sumeq2  11358  summodclem2  11381  divcnv  11496  prodeq2  11556  fprodsplitdc  11595  fprodconst  11619  dvdsle  11840  zsupcllemstep  11936  dvdsbnd  11947  gcdsupex  11948  gcdsupcl  11949  bezoutlemmain  11989  bezoutlemzz  11993  bezoutlembi  11996  dfgcd3  12001  dvdsmulgcd  12016  nnmindc  12025  lcmcllem  12057  lcmgcdlem  12067  ncoprmgcdne1b  12079  isprm5  12132  pw2dvdslemn  12155  oddpwdclemxy  12159  pythagtriplem2  12256  pythagtrip  12273  pceu  12285  pc2dvds  12319  pcz  12321  pcadd  12329  pcfac  12338  exmidunben  12417  ctiunctlemfo  12430  unct  12433  sgrpidmndm  12751  mndpropd  12771  mhmeql  12804  isgrpinv  12854  dfgrp3mlem  12896  mhmmnd  12908  issrg  13048  isring  13083  reldvdsrsrg  13160  dvdsrmul1  13170  tgrest  13451  cnpnei  13501  cnss1  13508  cncnp  13512  ismet2  13636  metequiv2  13778  metcnp  13794  metcnp2  13795  metcnpi3  13799  fsumcncntop  13838  elcncf2  13843  cncfmet  13861  suplociccreex  13884  dedekindicclemicc  13892  ivthinclemlr  13897  ivthinclemur  13899  cnplimclemr  13920  limccnpcntop  13926  limccoap  13929  lgsval2lem  14193  nninfalllem1  14528  sbthom  14545  apdiff  14567