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  6295  tfrlem1  6375  tfr1onlemaccex  6415  tfrcllemaccex  6428  frecabcl  6466  fopwdom  6906  phplem4dom  6932  phpm  6935  phplem4on  6937  fidifsnen  6940  diffisn  6963  diffifi  6964  en2eqpr  6977  fisseneq  7004  suplub2ti  7076  difinfsn  7175  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdc  7188  nninfninc  7198  nninfisol  7208  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  nninfwlpoimlemginf  7251  exmidontriimlem4  7309  exmidontriim  7310  cc3  7353  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  ltexnqq  7494  enq0tr  7520  addcmpblnq0  7529  mulcmpblnq0  7530  nnnq0lem1  7532  prssnqu  7566  prarloclemup  7581  nqprl  7637  nqpru  7638  mullocpr  7657  cauappcvgprlemladdfu  7740  cauappcvgprlemladdrl  7743  caucvgprlemm  7754  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlemlim  7767  caucvgprprlemml  7780  caucvgprprlemloc  7789  caucvgprprlemlim  7797  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  ltsrprg  7833  srpospr  7869  caucvgsrlemoffres  7886  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axcaucvglemcau  7984  axsuploc  8118  cnegexlem3  8222  negeu  8236  add20  8520  rimul  8631  apreap  8633  cru  8648  apreim  8649  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  apti  8668  aptap  8696  mulap0  8700  prodgt0  8898  ltmul12a  8906  ledivdiv  8936  lediv12a  8940  supinfneg  9688  infsupneg  9689  qapne  9732  xaddf  9938  xaddval  9939  xleadd1a  9967  xleaddadd  9981  ixxss12  10000  ioodisj  10087  fznlem  10135  zsupcllemstep  10338  qtri3or  10349  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  addmodlteq  10509  seqf1og  10632  mulexpzap  10690  leexp1a  10705  expnbnd  10774  apexp1  10829  faclbnd  10852  hashxp  10937  zfz1iso  10952  cjap  11090  caucvgre  11165  cvg1nlemres  11169  resqrexlemglsq  11206  resqrexlemga  11207  sqrtsq  11228  ltabs  11271  abs3lem  11295  cau3lem  11298  maxleim  11389  rexico  11405  minmax  11414  xrmaxleim  11428  xrmaxiflemcl  11429  xrmaxiflemlub  11432  xrmaxiflemval  11434  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  climcau  11531  climrecvg1n  11532  sumeq2  11543  summodclem2  11566  divcnv  11681  prodeq2  11741  fprodsplitdc  11780  fprodconst  11804  dvdsle  12028  bitsfzo  12139  dvdsbnd  12150  bezoutlemmain  12192  bezoutlemzz  12196  bezoutlembi  12199  dfgcd3  12204  dvdsmulgcd  12219  nnmindc  12228  lcmcllem  12262  lcmgcdlem  12272  ncoprmgcdne1b  12284  isprm5  12337  pw2dvdslemn  12360  oddpwdclemxy  12364  pythagtriplem2  12462  pythagtrip  12479  pceu  12491  pc2dvds  12526  pcz  12528  pcadd  12536  pcfac  12546  exmidunben  12670  ctiunctlemfo  12683  unct  12686  prdsval  12977  sgrppropd  13117  sgrpidmndm  13124  mndpropd  13144  mhmeql  13196  isgrpinv  13258  dfgrp3mlem  13302  mhmmnd  13324  conjnmzb  13488  ghmcmn  13535  gsumfzconst  13549  isrng  13568  issrg  13599  isring  13634  reldvdsrsrg  13726  dvdsrmul1  13736  tgrest  14513  cnpnei  14563  cnss1  14570  cncnp  14574  ismet2  14698  metequiv2  14840  metcnp  14856  metcnp2  14857  metcnpi3  14861  fsumcncntop  14911  elcncf2  14918  cncfmet  14936  suplociccreex  14968  dedekindicclemicc  14976  ivthinclemlr  14981  ivthinclemur  14983  cnplimclemr  15013  limccnpcntop  15019  limccoap  15022  dvmptfsum  15069  elply2  15079  plyrecj  15107  mersenne  15341  lgsval2lem  15359  lgsquad3  15433  nninfalllem1  15763  nnnninfex  15777  sbthom  15783  apdiff  15805