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  6344  tfrlem1  6424  tfr1onlemaccex  6464  tfrcllemaccex  6477  frecabcl  6515  fopwdom  6965  phplem4dom  6991  phpm  6995  phplem4on  6997  fidifsnen  7000  diffisn  7023  diffifi  7024  en2eqpr  7037  fisseneq  7064  suplub2ti  7136  difinfsn  7235  ctmlemr  7243  ctm  7244  ctssdclemn0  7245  ctssdc  7248  nninfninc  7258  nninfisol  7268  enomnilem  7273  enmkvlem  7296  enwomnilem  7304  nninfwlpoimlemginf  7311  exmidontriimlem4  7374  exmidontriim  7375  cc3  7422  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  ltexnqq  7563  enq0tr  7589  addcmpblnq0  7598  mulcmpblnq0  7599  nnnq0lem1  7601  prssnqu  7635  prarloclemup  7650  nqprl  7706  nqpru  7707  mullocpr  7726  cauappcvgprlemladdfu  7809  cauappcvgprlemladdrl  7812  caucvgprlemm  7823  caucvgprlemladdfu  7832  caucvgprlemladdrl  7833  caucvgprlemlim  7836  caucvgprprlemml  7849  caucvgprprlemloc  7858  caucvgprprlemlim  7866  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  ltsrprg  7902  srpospr  7938  caucvgsrlemoffres  7955  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  axcaucvglemcau  8053  axsuploc  8187  cnegexlem3  8291  negeu  8305  add20  8589  rimul  8700  apreap  8702  cru  8717  apreim  8718  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  apti  8737  aptap  8765  mulap0  8769  prodgt0  8967  ltmul12a  8975  ledivdiv  9005  lediv12a  9009  supinfneg  9758  infsupneg  9759  qapne  9802  xaddf  10008  xaddval  10009  xleadd1a  10037  xleaddadd  10051  ixxss12  10070  ioodisj  10157  fznlem  10205  zsupcllemstep  10416  qtri3or  10427  exbtwnzlemstep  10434  rebtwn2zlemstep  10439  addmodlteq  10587  seqf1og  10710  mulexpzap  10768  leexp1a  10783  expnbnd  10852  apexp1  10907  faclbnd  10930  hashxp  11015  zfz1iso  11030  swrdswrdlem  11202  cjap  11383  caucvgre  11458  cvg1nlemres  11462  resqrexlemglsq  11499  resqrexlemga  11500  sqrtsq  11521  ltabs  11564  abs3lem  11588  cau3lem  11591  maxleim  11682  rexico  11698  minmax  11707  xrmaxleim  11721  xrmaxiflemcl  11722  xrmaxiflemlub  11725  xrmaxiflemval  11727  xrmaxltsup  11735  xrmaxadd  11738  xrminmax  11742  xrbdtri  11753  climcau  11824  climrecvg1n  11825  sumeq2  11836  summodclem2  11859  divcnv  11974  prodeq2  12034  fprodsplitdc  12073  fprodconst  12097  dvdsle  12321  bitsfzo  12432  dvdsbnd  12443  bezoutlemmain  12485  bezoutlemzz  12489  bezoutlembi  12492  dfgcd3  12497  dvdsmulgcd  12512  nnmindc  12521  lcmcllem  12555  lcmgcdlem  12565  ncoprmgcdne1b  12577  isprm5  12630  pw2dvdslemn  12653  oddpwdclemxy  12657  pythagtriplem2  12755  pythagtrip  12772  pceu  12784  pc2dvds  12819  pcz  12821  pcadd  12829  pcfac  12839  exmidunben  12963  ctiunctlemfo  12976  unct  12979  prdsval  13272  sgrppropd  13412  sgrpidmndm  13419  mndpropd  13439  mhmeql  13491  isgrpinv  13553  dfgrp3mlem  13597  mhmmnd  13619  conjnmzb  13783  ghmcmn  13830  gsumfzconst  13844  isrng  13863  issrg  13894  isring  13929  reldvdsrsrg  14021  dvdsrmul1  14031  tgrest  14808  cnpnei  14858  cnss1  14865  cncnp  14869  ismet2  14993  metequiv2  15135  metcnp  15151  metcnp2  15152  metcnpi3  15156  fsumcncntop  15206  elcncf2  15213  cncfmet  15231  suplociccreex  15263  dedekindicclemicc  15271  ivthinclemlr  15276  ivthinclemur  15278  cnplimclemr  15308  limccnpcntop  15314  limccoap  15317  dvmptfsum  15364  elply2  15374  plyrecj  15402  mersenne  15636  lgsval2lem  15654  lgsquad3  15728  nninfalllem1  16285  nnnninfex  16299  sbthom  16305  apdiff  16327