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  6337  tfrlem1  6417  tfr1onlemaccex  6457  tfrcllemaccex  6470  frecabcl  6508  fopwdom  6958  phplem4dom  6984  phpm  6988  phplem4on  6990  fidifsnen  6993  diffisn  7016  diffifi  7017  en2eqpr  7030  fisseneq  7057  suplub2ti  7129  difinfsn  7228  ctmlemr  7236  ctm  7237  ctssdclemn0  7238  ctssdc  7241  nninfninc  7251  nninfisol  7261  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  nninfwlpoimlemginf  7304  exmidontriimlem4  7367  exmidontriim  7368  cc3  7415  addcmpblnq  7515  mulcmpblnq  7516  ordpipqqs  7522  ltexnqq  7556  enq0tr  7582  addcmpblnq0  7591  mulcmpblnq0  7592  nnnq0lem1  7594  prssnqu  7628  prarloclemup  7643  nqprl  7699  nqpru  7700  mullocpr  7719  cauappcvgprlemladdfu  7802  cauappcvgprlemladdrl  7805  caucvgprlemm  7816  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlemlim  7829  caucvgprprlemml  7842  caucvgprprlemloc  7851  caucvgprprlemlim  7859  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  addcmpblnr  7887  mulcmpblnrlemg  7888  mulcmpblnr  7889  ltsrprg  7895  srpospr  7931  caucvgsrlemoffres  7948  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axcaucvglemcau  8046  axsuploc  8180  cnegexlem3  8284  negeu  8298  add20  8582  rimul  8693  apreap  8695  cru  8710  apreim  8711  apsym  8714  apcotr  8715  apadd1  8716  apneg  8719  mulext1  8720  apti  8730  aptap  8758  mulap0  8762  prodgt0  8960  ltmul12a  8968  ledivdiv  8998  lediv12a  9002  supinfneg  9751  infsupneg  9752  qapne  9795  xaddf  10001  xaddval  10002  xleadd1a  10030  xleaddadd  10044  ixxss12  10063  ioodisj  10150  fznlem  10198  zsupcllemstep  10409  qtri3or  10420  exbtwnzlemstep  10427  rebtwn2zlemstep  10432  addmodlteq  10580  seqf1og  10703  mulexpzap  10761  leexp1a  10776  expnbnd  10845  apexp1  10900  faclbnd  10923  hashxp  11008  zfz1iso  11023  swrdswrdlem  11195  cjap  11332  caucvgre  11407  cvg1nlemres  11411  resqrexlemglsq  11448  resqrexlemga  11449  sqrtsq  11470  ltabs  11513  abs3lem  11537  cau3lem  11540  maxleim  11631  rexico  11647  minmax  11656  xrmaxleim  11670  xrmaxiflemcl  11671  xrmaxiflemlub  11674  xrmaxiflemval  11676  xrmaxltsup  11684  xrmaxadd  11687  xrminmax  11691  xrbdtri  11702  climcau  11773  climrecvg1n  11774  sumeq2  11785  summodclem2  11808  divcnv  11923  prodeq2  11983  fprodsplitdc  12022  fprodconst  12046  dvdsle  12270  bitsfzo  12381  dvdsbnd  12392  bezoutlemmain  12434  bezoutlemzz  12438  bezoutlembi  12441  dfgcd3  12446  dvdsmulgcd  12461  nnmindc  12470  lcmcllem  12504  lcmgcdlem  12514  ncoprmgcdne1b  12526  isprm5  12579  pw2dvdslemn  12602  oddpwdclemxy  12606  pythagtriplem2  12704  pythagtrip  12721  pceu  12733  pc2dvds  12768  pcz  12770  pcadd  12778  pcfac  12788  exmidunben  12912  ctiunctlemfo  12925  unct  12928  prdsval  13220  sgrppropd  13360  sgrpidmndm  13367  mndpropd  13387  mhmeql  13439  isgrpinv  13501  dfgrp3mlem  13545  mhmmnd  13567  conjnmzb  13731  ghmcmn  13778  gsumfzconst  13792  isrng  13811  issrg  13842  isring  13877  reldvdsrsrg  13969  dvdsrmul1  13979  tgrest  14756  cnpnei  14806  cnss1  14813  cncnp  14817  ismet2  14941  metequiv2  15083  metcnp  15099  metcnp2  15100  metcnpi3  15104  fsumcncntop  15154  elcncf2  15161  cncfmet  15179  suplociccreex  15211  dedekindicclemicc  15219  ivthinclemlr  15224  ivthinclemur  15226  cnplimclemr  15256  limccnpcntop  15262  limccoap  15265  dvmptfsum  15312  elply2  15322  plyrecj  15350  mersenne  15584  lgsval2lem  15602  lgsquad3  15676  nninfalllem1  16147  nnnninfex  16161  sbthom  16167  apdiff  16189