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  6398  tfrlem1  6479  tfr1onlemaccex  6519  tfrcllemaccex  6532  frecabcl  6570  fopwdom  7027  phplem4dom  7053  phpm  7057  phplem4on  7059  fidifsnen  7062  diffisn  7087  diffifi  7088  en2eqpr  7104  fisseneq  7132  suplub2ti  7205  difinfsn  7304  ctmlemr  7312  ctm  7313  ctssdclemn0  7314  ctssdc  7317  nninfninc  7327  nninfisol  7337  enomnilem  7342  enmkvlem  7365  enwomnilem  7373  nninfwlpoimlemginf  7380  exmidontriimlem4  7444  exmidontriim  7445  cc3  7492  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  ltexnqq  7633  enq0tr  7659  addcmpblnq0  7668  mulcmpblnq0  7669  nnnq0lem1  7671  prssnqu  7705  prarloclemup  7720  nqprl  7776  nqpru  7777  mullocpr  7796  cauappcvgprlemladdfu  7879  cauappcvgprlemladdrl  7882  caucvgprlemm  7893  caucvgprlemladdfu  7902  caucvgprlemladdrl  7903  caucvgprlemlim  7906  caucvgprprlemml  7919  caucvgprprlemloc  7928  caucvgprprlemlim  7936  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemdisj  7945  suplocexprlemloc  7946  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  ltsrprg  7972  srpospr  8008  caucvgsrlemoffres  8025  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  axcaucvglemcau  8123  axsuploc  8257  cnegexlem3  8361  negeu  8375  add20  8659  rimul  8770  apreap  8772  cru  8787  apreim  8788  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  apti  8807  aptap  8835  mulap0  8839  prodgt0  9037  ltmul12a  9045  ledivdiv  9075  lediv12a  9079  supinfneg  9834  infsupneg  9835  qapne  9878  xaddf  10084  xaddval  10085  xleadd1a  10113  xleaddadd  10127  ixxss12  10146  ioodisj  10233  fznlem  10281  zsupcllemstep  10495  qtri3or  10506  exbtwnzlemstep  10513  rebtwn2zlemstep  10518  addmodlteq  10666  seqf1og  10789  mulexpzap  10847  leexp1a  10862  expnbnd  10931  apexp1  10986  faclbnd  11009  hashxp  11096  zfz1iso  11111  swrdswrdlem  11294  cjap  11489  caucvgre  11564  cvg1nlemres  11568  resqrexlemglsq  11605  resqrexlemga  11606  sqrtsq  11627  ltabs  11670  abs3lem  11694  cau3lem  11697  maxleim  11788  rexico  11804  minmax  11813  xrmaxleim  11827  xrmaxiflemcl  11828  xrmaxiflemlub  11831  xrmaxiflemval  11833  xrmaxltsup  11841  xrmaxadd  11844  xrminmax  11848  xrbdtri  11859  climcau  11930  climrecvg1n  11931  sumeq2  11942  summodclem2  11966  divcnv  12081  prodeq2  12141  fprodsplitdc  12180  fprodconst  12204  dvdsle  12428  bitsfzo  12539  dvdsbnd  12550  bezoutlemmain  12592  bezoutlemzz  12596  bezoutlembi  12599  dfgcd3  12604  dvdsmulgcd  12619  nnmindc  12628  lcmcllem  12662  lcmgcdlem  12672  ncoprmgcdne1b  12684  isprm5  12737  pw2dvdslemn  12760  oddpwdclemxy  12764  pythagtriplem2  12862  pythagtrip  12879  pceu  12891  pc2dvds  12926  pcz  12928  pcadd  12936  pcfac  12946  exmidunben  13070  ctiunctlemfo  13083  unct  13086  prdsval  13379  sgrppropd  13519  sgrpidmndm  13526  mndpropd  13546  mhmeql  13598  isgrpinv  13660  dfgrp3mlem  13704  mhmmnd  13726  conjnmzb  13890  ghmcmn  13937  gsumfzconst  13951  isrng  13971  issrg  14002  isring  14037  dvdsrmul1  14140  tgrest  14922  cnpnei  14972  cnss1  14979  cncnp  14983  ismet2  15107  metequiv2  15249  metcnp  15265  metcnp2  15266  metcnpi3  15270  fsumcncntop  15320  elcncf2  15327  cncfmet  15345  suplociccreex  15377  dedekindicclemicc  15385  ivthinclemlr  15390  ivthinclemur  15392  cnplimclemr  15422  limccnpcntop  15428  limccoap  15431  dvmptfsum  15478  elply2  15488  plyrecj  15516  mersenne  15750  lgsval2lem  15768  lgsquad3  15842  usgr1eop  16125  usgr1vr  16128  pw1ndom3  16649  nninfalllem1  16673  nnnninfex  16687  sbthom  16693  apdiff  16719