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  6388  tfrlem1  6469  tfr1onlemaccex  6509  tfrcllemaccex  6522  frecabcl  6560  fopwdom  7017  phplem4dom  7043  phpm  7047  phplem4on  7049  fidifsnen  7052  diffisn  7077  diffifi  7078  en2eqpr  7094  fisseneq  7121  suplub2ti  7194  difinfsn  7293  ctmlemr  7301  ctm  7302  ctssdclemn0  7303  ctssdc  7306  nninfninc  7316  nninfisol  7326  enomnilem  7331  enmkvlem  7354  enwomnilem  7362  nninfwlpoimlemginf  7369  exmidontriimlem4  7432  exmidontriim  7433  cc3  7480  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  ltexnqq  7621  enq0tr  7647  addcmpblnq0  7656  mulcmpblnq0  7657  nnnq0lem1  7659  prssnqu  7693  prarloclemup  7708  nqprl  7764  nqpru  7765  mullocpr  7784  cauappcvgprlemladdfu  7867  cauappcvgprlemladdrl  7870  caucvgprlemm  7881  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgprlemlim  7894  caucvgprprlemml  7907  caucvgprprlemloc  7916  caucvgprprlemlim  7924  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  ltsrprg  7960  srpospr  7996  caucvgsrlemoffres  8013  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  axcaucvglemcau  8111  axsuploc  8245  cnegexlem3  8349  negeu  8363  add20  8647  rimul  8758  apreap  8760  cru  8775  apreim  8776  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  apti  8795  aptap  8823  mulap0  8827  prodgt0  9025  ltmul12a  9033  ledivdiv  9063  lediv12a  9067  supinfneg  9822  infsupneg  9823  qapne  9866  xaddf  10072  xaddval  10073  xleadd1a  10101  xleaddadd  10115  ixxss12  10134  ioodisj  10221  fznlem  10269  zsupcllemstep  10482  qtri3or  10493  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  addmodlteq  10653  seqf1og  10776  mulexpzap  10834  leexp1a  10849  expnbnd  10918  apexp1  10973  faclbnd  10996  hashxp  11083  zfz1iso  11098  swrdswrdlem  11278  cjap  11460  caucvgre  11535  cvg1nlemres  11539  resqrexlemglsq  11576  resqrexlemga  11577  sqrtsq  11598  ltabs  11641  abs3lem  11665  cau3lem  11668  maxleim  11759  rexico  11775  minmax  11784  xrmaxleim  11798  xrmaxiflemcl  11799  xrmaxiflemlub  11802  xrmaxiflemval  11804  xrmaxltsup  11812  xrmaxadd  11815  xrminmax  11819  xrbdtri  11830  climcau  11901  climrecvg1n  11902  sumeq2  11913  summodclem2  11936  divcnv  12051  prodeq2  12111  fprodsplitdc  12150  fprodconst  12174  dvdsle  12398  bitsfzo  12509  dvdsbnd  12520  bezoutlemmain  12562  bezoutlemzz  12566  bezoutlembi  12569  dfgcd3  12574  dvdsmulgcd  12589  nnmindc  12598  lcmcllem  12632  lcmgcdlem  12642  ncoprmgcdne1b  12654  isprm5  12707  pw2dvdslemn  12730  oddpwdclemxy  12734  pythagtriplem2  12832  pythagtrip  12849  pceu  12861  pc2dvds  12896  pcz  12898  pcadd  12906  pcfac  12916  exmidunben  13040  ctiunctlemfo  13053  unct  13056  prdsval  13349  sgrppropd  13489  sgrpidmndm  13496  mndpropd  13516  mhmeql  13568  isgrpinv  13630  dfgrp3mlem  13674  mhmmnd  13696  conjnmzb  13860  ghmcmn  13907  gsumfzconst  13921  isrng  13940  issrg  13971  isring  14006  dvdsrmul1  14109  tgrest  14886  cnpnei  14936  cnss1  14943  cncnp  14947  ismet2  15071  metequiv2  15213  metcnp  15229  metcnp2  15230  metcnpi3  15234  fsumcncntop  15284  elcncf2  15291  cncfmet  15309  suplociccreex  15341  dedekindicclemicc  15349  ivthinclemlr  15354  ivthinclemur  15356  cnplimclemr  15386  limccnpcntop  15392  limccoap  15395  dvmptfsum  15442  elply2  15452  plyrecj  15480  mersenne  15714  lgsval2lem  15732  lgsquad3  15806  usgr1eop  16089  usgr1vr  16092  pw1ndom3  16539  nninfalllem1  16560  nnnninfex  16574  sbthom  16580  apdiff  16602