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  6321  tfrlem1  6401  tfr1onlemaccex  6441  tfrcllemaccex  6454  frecabcl  6492  fopwdom  6940  phplem4dom  6966  phpm  6969  phplem4on  6971  fidifsnen  6974  diffisn  6997  diffifi  6998  en2eqpr  7011  fisseneq  7038  suplub2ti  7110  difinfsn  7209  ctmlemr  7217  ctm  7218  ctssdclemn0  7219  ctssdc  7222  nninfninc  7232  nninfisol  7242  enomnilem  7247  enmkvlem  7270  enwomnilem  7278  nninfwlpoimlemginf  7285  exmidontriimlem4  7343  exmidontriim  7344  cc3  7387  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  ltexnqq  7528  enq0tr  7554  addcmpblnq0  7563  mulcmpblnq0  7564  nnnq0lem1  7566  prssnqu  7600  prarloclemup  7615  nqprl  7671  nqpru  7672  mullocpr  7691  cauappcvgprlemladdfu  7774  cauappcvgprlemladdrl  7777  caucvgprlemm  7788  caucvgprlemladdfu  7797  caucvgprlemladdrl  7798  caucvgprlemlim  7801  caucvgprprlemml  7814  caucvgprprlemloc  7823  caucvgprprlemlim  7831  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  ltsrprg  7867  srpospr  7903  caucvgsrlemoffres  7920  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  axcaucvglemcau  8018  axsuploc  8152  cnegexlem3  8256  negeu  8270  add20  8554  rimul  8665  apreap  8667  cru  8682  apreim  8683  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  apti  8702  aptap  8730  mulap0  8734  prodgt0  8932  ltmul12a  8940  ledivdiv  8970  lediv12a  8974  supinfneg  9723  infsupneg  9724  qapne  9767  xaddf  9973  xaddval  9974  xleadd1a  10002  xleaddadd  10016  ixxss12  10035  ioodisj  10122  fznlem  10170  zsupcllemstep  10379  qtri3or  10390  exbtwnzlemstep  10397  rebtwn2zlemstep  10402  addmodlteq  10550  seqf1og  10673  mulexpzap  10731  leexp1a  10746  expnbnd  10815  apexp1  10870  faclbnd  10893  hashxp  10978  zfz1iso  10993  swrdswrdlem  11163  cjap  11261  caucvgre  11336  cvg1nlemres  11340  resqrexlemglsq  11377  resqrexlemga  11378  sqrtsq  11399  ltabs  11442  abs3lem  11466  cau3lem  11469  maxleim  11560  rexico  11576  minmax  11585  xrmaxleim  11599  xrmaxiflemcl  11600  xrmaxiflemlub  11603  xrmaxiflemval  11605  xrmaxltsup  11613  xrmaxadd  11616  xrminmax  11620  xrbdtri  11631  climcau  11702  climrecvg1n  11703  sumeq2  11714  summodclem2  11737  divcnv  11852  prodeq2  11912  fprodsplitdc  11951  fprodconst  11975  dvdsle  12199  bitsfzo  12310  dvdsbnd  12321  bezoutlemmain  12363  bezoutlemzz  12367  bezoutlembi  12370  dfgcd3  12375  dvdsmulgcd  12390  nnmindc  12399  lcmcllem  12433  lcmgcdlem  12443  ncoprmgcdne1b  12455  isprm5  12508  pw2dvdslemn  12531  oddpwdclemxy  12535  pythagtriplem2  12633  pythagtrip  12650  pceu  12662  pc2dvds  12697  pcz  12699  pcadd  12707  pcfac  12717  exmidunben  12841  ctiunctlemfo  12854  unct  12857  prdsval  13149  sgrppropd  13289  sgrpidmndm  13296  mndpropd  13316  mhmeql  13368  isgrpinv  13430  dfgrp3mlem  13474  mhmmnd  13496  conjnmzb  13660  ghmcmn  13707  gsumfzconst  13721  isrng  13740  issrg  13771  isring  13806  reldvdsrsrg  13898  dvdsrmul1  13908  tgrest  14685  cnpnei  14735  cnss1  14742  cncnp  14746  ismet2  14870  metequiv2  15012  metcnp  15028  metcnp2  15029  metcnpi3  15033  fsumcncntop  15083  elcncf2  15090  cncfmet  15108  suplociccreex  15140  dedekindicclemicc  15148  ivthinclemlr  15153  ivthinclemur  15155  cnplimclemr  15185  limccnpcntop  15191  limccoap  15194  dvmptfsum  15241  elply2  15251  plyrecj  15279  mersenne  15513  lgsval2lem  15531  lgsquad3  15605  nninfalllem1  16019  nnnninfex  16033  sbthom  16039  apdiff  16061