Theorem simpllr 540

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 492	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4r  548  f1o2ndf1  6464  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  fopwdom  7136  phplem4dom  7163  phpm  7167  phplem4on  7169  fidifsnen  7172  diffisn  7197  diffifi  7198  en2eqpr  7214  fisseneq  7242  suplub2ti  7341  difinfsn  7440  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdc  7453  nninfninc  7463  nninfisol  7473  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemginf  7516  exmidontriimlem4  7580  exmidontriim  7581  cc3  7634  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  ltexnqq  7775  enq0tr  7801  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prssnqu  7847  prarloclemup  7862  nqprl  7918  nqpru  7919  mullocpr  7938  cauappcvgprlemladdfu  8021  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemloc  8070  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  srpospr  8150  caucvgsrlemoffres  8167  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axsuploc  8398  cnegexlem3  8503  negeu  8517  add20  8802  rimul  8914  apreap  8916  cru  8931  apreim  8932  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  apti  8951  aptap  8979  mulap0  8983  prodgt0  9183  ltmul12a  9191  ledivdiv  9221  lediv12a  9225  supinfneg  9997  infsupneg  9998  qapne  10041  xaddf  10248  xaddval  10249  xleadd1a  10277  xleaddadd  10291  ixxss12  10310  ioodisj  10397  fznlem  10447  zsupcllemstep  10664  qtri3or  10677  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  addmodlteq  10837  seqf1og  10960  mulexpzap  11018  leexp1a  11033  expnbnd  11103  apexp1  11158  faclbnd  11181  hashxp  11269  sshashneg  11283  hashf1lem2  11288  zfz1iso  11295  swrdswrdlem  11478  cjap  11674  caucvgre  11749  cvg1nlemres  11753  resqrexlemglsq  11790  resqrexlemga  11791  sqrtsq  11812  ltabs  11855  abs3lem  11879  cau3lem  11882  maxleim  11973  rexico  11989  minmax  11998  xrmaxleim  12012  xrmaxiflemcl  12013  xrmaxiflemlub  12016  xrmaxiflemval  12018  xrmaxltsup  12026  xrmaxadd  12029  xrminmax  12033  xrbdtri  12044  climcau  12115  climrecvg1n  12116  sumeq2  12127  summodclem2  12151  divcnv  12266  prodeq2  12326  fprodsplitdc  12365  fprodconst  12389  dvdsle  12613  bitsfzo  12724  dvdsbnd  12735  bezoutlemmain  12777  bezoutlemzz  12781  bezoutlembi  12784  dfgcd3  12789  dvdsmulgcd  12804  nnmindc  12813  lcmcllem  12847  lcmgcdlem  12857  ncoprmgcdne1b  12869  isprm5  12922  pw2dvdslemn  12945  oddpwdclemxy  12949  pythagtriplem2  13047  pythagtrip  13064  pceu  13076  pc2dvds  13111  pcz  13113  pcadd  13121  pcfac  13131  exmidunben  13319  ctiunctlemfo  13332  unct  13335  sgrppropd  13730  sgrpidmndm  13735  mndpropd  13755  mhmeql  13801  isgrpinv  13861  dfgrp3mlem  13905  mhmmnd  13921  conjnmzb  14085  ghmcmn  14133  gzsumconst  14145  prdsval  14175  isrng  14235  issrg  14271  isring  14306  dvdsrmul1  14411  aprlring  14602  issubassa2  15037  tgrest  15272  cnpnei  15322  cnss1  15329  cncnp  15333  ismet2  15457  metequiv2  15599  metcnp  15615  metcnp2  15616  metcnpi3  15620  fsumcncntop  15670  elcncf2  15677  cncfmet  15695  suplociccreex  15727  dedekindicclemicc  15735  ivthinclemlr  15740  ivthinclemur  15742  cnplimclemr  15772  limccnpcntop  15778  limccoap  15781  dvmptfsum  15828  elply2  15838  plyrecj  15866  logdivlt  15999  mersenne  16117  lgsval2lem  16141  lgsquad3  16215  usgr1eop  16498  usgr1vr  16501  pw1ndom3  17032  nninfalllem1  17063  nnnninfex  17077  sbthom  17083  apdiff  17109