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  6229  tfrlem1  6309  tfr1onlemaccex  6349  tfrcllemaccex  6362  frecabcl  6400  fopwdom  6836  phplem4dom  6862  phpm  6865  phplem4on  6867  fidifsnen  6870  diffisn  6893  diffifi  6894  en2eqpr  6907  fisseneq  6931  suplub2ti  7000  difinfsn  7099  ctmlemr  7107  ctm  7108  ctssdclemn0  7109  ctssdc  7112  nninfisol  7131  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  nninfwlpoimlemginf  7174  exmidontriimlem4  7223  exmidontriim  7224  cc3  7267  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  ltexnqq  7407  enq0tr  7433  addcmpblnq0  7442  mulcmpblnq0  7443  nnnq0lem1  7445  prssnqu  7479  prarloclemup  7494  nqprl  7550  nqpru  7551  mullocpr  7570  cauappcvgprlemladdfu  7653  cauappcvgprlemladdrl  7656  caucvgprlemm  7667  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlemlim  7680  caucvgprprlemml  7693  caucvgprprlemloc  7702  caucvgprprlemlim  7710  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  ltsrprg  7746  srpospr  7782  caucvgsrlemoffres  7799  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axcaucvglemcau  7897  axsuploc  8030  cnegexlem3  8134  negeu  8148  add20  8431  rimul  8542  apreap  8544  cru  8559  apreim  8560  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  apti  8579  aptap  8607  mulap0  8611  prodgt0  8809  ltmul12a  8817  ledivdiv  8847  lediv12a  8851  supinfneg  9595  infsupneg  9596  qapne  9639  xaddf  9844  xaddval  9845  xleadd1a  9873  xleaddadd  9887  ixxss12  9906  ioodisj  9993  fznlem  10041  qtri3or  10243  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  addmodlteq  10398  mulexpzap  10560  leexp1a  10575  expnbnd  10644  apexp1  10698  faclbnd  10721  hashxp  10806  zfz1iso  10821  cjap  10915  caucvgre  10990  cvg1nlemres  10994  resqrexlemglsq  11031  resqrexlemga  11032  sqrtsq  11053  ltabs  11096  abs3lem  11120  cau3lem  11123  maxleim  11214  rexico  11230  minmax  11238  xrmaxleim  11252  xrmaxiflemcl  11253  xrmaxiflemlub  11256  xrmaxiflemval  11258  xrmaxltsup  11266  xrmaxadd  11269  xrminmax  11273  xrbdtri  11284  climcau  11355  climrecvg1n  11356  sumeq2  11367  summodclem2  11390  divcnv  11505  prodeq2  11565  fprodsplitdc  11604  fprodconst  11628  dvdsle  11850  zsupcllemstep  11946  dvdsbnd  11957  gcdsupex  11958  gcdsupcl  11959  bezoutlemmain  11999  bezoutlemzz  12003  bezoutlembi  12006  dfgcd3  12011  dvdsmulgcd  12026  nnmindc  12035  lcmcllem  12067  lcmgcdlem  12077  ncoprmgcdne1b  12089  isprm5  12142  pw2dvdslemn  12165  oddpwdclemxy  12169  pythagtriplem2  12266  pythagtrip  12283  pceu  12295  pc2dvds  12329  pcz  12331  pcadd  12339  pcfac  12348  exmidunben  12427  ctiunctlemfo  12440  unct  12443  sgrpidmndm  12821  mndpropd  12841  mhmeql  12876  isgrpinv  12926  dfgrp3mlem  12968  mhmmnd  12980  issrg  13148  isring  13183  reldvdsrsrg  13261  dvdsrmul1  13271  tgrest  13672  cnpnei  13722  cnss1  13729  cncnp  13733  ismet2  13857  metequiv2  13999  metcnp  14015  metcnp2  14016  metcnpi3  14020  fsumcncntop  14059  elcncf2  14064  cncfmet  14082  suplociccreex  14105  dedekindicclemicc  14113  ivthinclemlr  14118  ivthinclemur  14120  cnplimclemr  14141  limccnpcntop  14147  limccoap  14150  lgsval2lem  14414  nninfalllem1  14760  sbthom  14777  apdiff  14799