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  6283  tfrlem1  6363  tfr1onlemaccex  6403  tfrcllemaccex  6416  frecabcl  6454  fopwdom  6894  phplem4dom  6920  phpm  6923  phplem4on  6925  fidifsnen  6928  diffisn  6951  diffifi  6952  en2eqpr  6965  fisseneq  6990  suplub2ti  7062  difinfsn  7161  ctmlemr  7169  ctm  7170  ctssdclemn0  7171  ctssdc  7174  nninfninc  7184  nninfisol  7194  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  nninfwlpoimlemginf  7237  exmidontriimlem4  7286  exmidontriim  7287  cc3  7330  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  ltexnqq  7470  enq0tr  7496  addcmpblnq0  7505  mulcmpblnq0  7506  nnnq0lem1  7508  prssnqu  7542  prarloclemup  7557  nqprl  7613  nqpru  7614  mullocpr  7633  cauappcvgprlemladdfu  7716  cauappcvgprlemladdrl  7719  caucvgprlemm  7730  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlemlim  7743  caucvgprprlemml  7756  caucvgprprlemloc  7765  caucvgprprlemlim  7773  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  ltsrprg  7809  srpospr  7845  caucvgsrlemoffres  7862  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axcaucvglemcau  7960  axsuploc  8094  cnegexlem3  8198  negeu  8212  add20  8495  rimul  8606  apreap  8608  cru  8623  apreim  8624  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  apti  8643  aptap  8671  mulap0  8675  prodgt0  8873  ltmul12a  8881  ledivdiv  8911  lediv12a  8915  supinfneg  9663  infsupneg  9664  qapne  9707  xaddf  9913  xaddval  9914  xleadd1a  9942  xleaddadd  9956  ixxss12  9975  ioodisj  10062  fznlem  10110  qtri3or  10313  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  addmodlteq  10472  seqf1og  10595  mulexpzap  10653  leexp1a  10668  expnbnd  10737  apexp1  10792  faclbnd  10815  hashxp  10900  zfz1iso  10915  cjap  11053  caucvgre  11128  cvg1nlemres  11132  resqrexlemglsq  11169  resqrexlemga  11170  sqrtsq  11191  ltabs  11234  abs3lem  11258  cau3lem  11261  maxleim  11352  rexico  11368  minmax  11376  xrmaxleim  11390  xrmaxiflemcl  11391  xrmaxiflemlub  11394  xrmaxiflemval  11396  xrmaxltsup  11404  xrmaxadd  11407  xrminmax  11411  xrbdtri  11422  climcau  11493  climrecvg1n  11494  sumeq2  11505  summodclem2  11528  divcnv  11643  prodeq2  11703  fprodsplitdc  11742  fprodconst  11766  dvdsle  11989  zsupcllemstep  12085  dvdsbnd  12096  bezoutlemmain  12138  bezoutlemzz  12142  bezoutlembi  12145  dfgcd3  12150  dvdsmulgcd  12165  nnmindc  12174  lcmcllem  12208  lcmgcdlem  12218  ncoprmgcdne1b  12230  isprm5  12283  pw2dvdslemn  12306  oddpwdclemxy  12310  pythagtriplem2  12407  pythagtrip  12424  pceu  12436  pc2dvds  12471  pcz  12473  pcadd  12481  pcfac  12491  exmidunben  12586  ctiunctlemfo  12599  unct  12602  sgrppropd  12999  sgrpidmndm  13004  mndpropd  13024  mhmeql  13067  isgrpinv  13129  dfgrp3mlem  13173  mhmmnd  13189  conjnmzb  13353  ghmcmn  13400  gsumfzconst  13414  isrng  13433  issrg  13464  isring  13499  reldvdsrsrg  13591  dvdsrmul1  13601  tgrest  14348  cnpnei  14398  cnss1  14405  cncnp  14409  ismet2  14533  metequiv2  14675  metcnp  14691  metcnp2  14692  metcnpi3  14696  fsumcncntop  14746  elcncf2  14753  cncfmet  14771  suplociccreex  14803  dedekindicclemicc  14811  ivthinclemlr  14816  ivthinclemur  14818  cnplimclemr  14848  limccnpcntop  14854  limccoap  14857  dvmptfsum  14904  elply2  14914  plyrecj  14941  lgsval2lem  15167  lgsquad3  15241  nninfalllem1  15568  sbthom  15586  apdiff  15608