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  6437  tfrlem1  6552  tfr1onlemaccex  6592  tfrcllemaccex  6605  frecabcl  6643  fopwdom  7102  phplem4dom  7129  phpm  7133  phplem4on  7135  fidifsnen  7138  diffisn  7163  diffifi  7164  en2eqpr  7180  fisseneq  7208  suplub2ti  7305  difinfsn  7404  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdc  7417  nninfninc  7427  nninfisol  7437  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  nninfwlpoimlemginf  7480  exmidontriimlem4  7544  exmidontriim  7545  cc3  7598  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prssnqu  7811  prarloclemup  7826  nqprl  7882  nqpru  7883  mullocpr  7902  cauappcvgprlemladdfu  7985  cauappcvgprlemladdrl  7988  caucvgprlemm  7999  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemloc  8034  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  srpospr  8114  caucvgsrlemoffres  8131  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axsuploc  8362  cnegexlem3  8467  negeu  8481  add20  8766  rimul  8877  apreap  8879  cru  8894  apreim  8895  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  apti  8914  aptap  8942  mulap0  8946  prodgt0  9146  ltmul12a  9154  ledivdiv  9184  lediv12a  9188  supinfneg  9948  infsupneg  9949  qapne  9992  xaddf  10199  xaddval  10200  xleadd1a  10228  xleaddadd  10242  ixxss12  10261  ioodisj  10348  fznlem  10398  zsupcllemstep  10614  qtri3or  10627  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  addmodlteq  10787  seqf1og  10910  mulexpzap  10968  leexp1a  10983  expnbnd  11053  apexp1  11108  faclbnd  11131  hashxp  11219  sshashneg  11233  zfz1iso  11241  swrdswrdlem  11424  cjap  11619  caucvgre  11694  cvg1nlemres  11698  resqrexlemglsq  11735  resqrexlemga  11736  sqrtsq  11757  ltabs  11800  abs3lem  11824  cau3lem  11827  maxleim  11918  rexico  11934  minmax  11943  xrmaxleim  11957  xrmaxiflemcl  11958  xrmaxiflemlub  11961  xrmaxiflemval  11963  xrmaxltsup  11971  xrmaxadd  11974  xrminmax  11978  xrbdtri  11989  climcau  12060  climrecvg1n  12061  sumeq2  12072  summodclem2  12096  divcnv  12211  prodeq2  12271  fprodsplitdc  12310  fprodconst  12334  dvdsle  12558  bitsfzo  12669  dvdsbnd  12680  bezoutlemmain  12722  bezoutlemzz  12726  bezoutlembi  12729  dfgcd3  12734  dvdsmulgcd  12749  nnmindc  12758  lcmcllem  12792  lcmgcdlem  12802  ncoprmgcdne1b  12814  isprm5  12867  pw2dvdslemn  12890  oddpwdclemxy  12894  pythagtriplem2  12992  pythagtrip  13009  pceu  13021  pc2dvds  13056  pcz  13058  pcadd  13066  pcfac  13076  exmidunben  13264  ctiunctlemfo  13277  unct  13280  sgrppropd  13679  sgrpidmndm  13684  mndpropd  13704  mhmeql  13750  isgrpinv  13812  dfgrp3mlem  13856  mhmmnd  13872  conjnmzb  14036  ghmcmn  14083  gsumfzconst  14097  prdsval  14118  isrng  14176  issrg  14211  isring  14246  dvdsrmul1  14350  aprlring  14541  tgrest  15163  cnpnei  15213  cnss1  15220  cncnp  15224  ismet2  15348  metequiv2  15490  metcnp  15506  metcnp2  15507  metcnpi3  15511  fsumcncntop  15561  elcncf2  15568  cncfmet  15586  suplociccreex  15618  dedekindicclemicc  15626  ivthinclemlr  15631  ivthinclemur  15633  cnplimclemr  15663  limccnpcntop  15669  limccoap  15672  dvmptfsum  15719  elply2  15729  plyrecj  15757  mersenne  15994  lgsval2lem  16012  lgsquad3  16086  usgr1eop  16369  usgr1vr  16372  pw1ndom3  16903  nninfalllem1  16925  nnnninfex  16939  sbthom  16945  apdiff  16971  trimul0or  16984