Theorem simpllr 524

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 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 480	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4r  532  f1o2ndf1  6187  tfrlem1  6267  tfr1onlemaccex  6307  tfrcllemaccex  6320  frecabcl  6358  fopwdom  6793  phplem4dom  6819  phpm  6822  phplem4on  6824  fidifsnen  6827  diffisn  6850  diffifi  6851  en2eqpr  6864  fisseneq  6888  suplub2ti  6957  difinfsn  7056  ctmlemr  7064  ctm  7065  ctssdclemn0  7066  ctssdc  7069  nninfisol  7088  enomnilem  7093  enmkvlem  7116  enwomnilem  7124  exmidontriimlem4  7171  exmidontriim  7172  cc3  7200  addcmpblnq  7299  mulcmpblnq  7300  ordpipqqs  7306  ltexnqq  7340  enq0tr  7366  addcmpblnq0  7375  mulcmpblnq0  7376  nnnq0lem1  7378  prssnqu  7412  prarloclemup  7427  nqprl  7483  nqpru  7484  mullocpr  7503  cauappcvgprlemladdfu  7586  cauappcvgprlemladdrl  7589  caucvgprlemm  7600  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlemlim  7613  caucvgprprlemml  7626  caucvgprprlemloc  7635  caucvgprprlemlim  7643  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemloc  7653  addcmpblnr  7671  mulcmpblnrlemg  7672  mulcmpblnr  7673  ltsrprg  7679  srpospr  7715  caucvgsrlemoffres  7732  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  axcaucvglemcau  7830  axsuploc  7962  cnegexlem3  8066  negeu  8080  add20  8363  rimul  8474  apreap  8476  cru  8491  apreim  8492  apsym  8495  apcotr  8496  apadd1  8497  apneg  8500  mulext1  8501  apti  8511  mulap0  8542  prodgt0  8738  ltmul12a  8746  ledivdiv  8776  lediv12a  8780  supinfneg  9524  infsupneg  9525  qapne  9568  xaddf  9771  xaddval  9772  xleadd1a  9800  xleaddadd  9814  ixxss12  9833  ioodisj  9920  fznlem  9966  qtri3or  10168  exbtwnzlemstep  10173  rebtwn2zlemstep  10178  addmodlteq  10323  mulexpzap  10485  leexp1a  10500  expnbnd  10567  apexp1  10620  faclbnd  10643  hashxp  10728  zfz1iso  10740  cjap  10834  caucvgre  10909  cvg1nlemres  10913  resqrexlemglsq  10950  resqrexlemga  10951  sqrtsq  10972  ltabs  11015  abs3lem  11039  cau3lem  11042  maxleim  11133  rexico  11149  minmax  11157  xrmaxleim  11171  xrmaxiflemcl  11172  xrmaxiflemlub  11175  xrmaxiflemval  11177  xrmaxltsup  11185  xrmaxadd  11188  xrminmax  11192  xrbdtri  11203  climcau  11274  climrecvg1n  11275  sumeq2  11286  summodclem2  11309  divcnv  11424  prodeq2  11484  fprodsplitdc  11523  fprodconst  11547  dvdsle  11767  zsupcllemstep  11863  dvdsbnd  11874  gcdsupex  11875  gcdsupcl  11876  bezoutlemmain  11916  bezoutlemzz  11920  bezoutlembi  11923  dfgcd3  11928  dvdsmulgcd  11943  lcmcllem  11978  lcmgcdlem  11988  ncoprmgcdne1b  12000  pw2dvdslemn  12074  oddpwdclemxy  12078  pythagtriplem2  12175  pythagtrip  12192  pceu  12204  pc2dvds  12238  pcz  12240  pcadd  12248  pcfac  12257  exmidunben  12296  ctiunctlemfo  12309  unct  12312  nnmindc  12318  tgrest  12710  cnpnei  12760  cnss1  12767  cncnp  12771  ismet2  12895  metequiv2  13037  metcnp  13053  metcnp2  13054  metcnpi3  13058  fsumcncntop  13097  elcncf2  13102  cncfmet  13120  suplociccreex  13143  dedekindicclemicc  13151  ivthinclemlr  13156  ivthinclemur  13158  cnplimclemr  13179  limccnpcntop  13185  limccoap  13188  nninfalllem1  13722  sbthom  13739  apdiff  13761