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  6385  tfrlem1  6465  tfr1onlemaccex  6505  tfrcllemaccex  6518  frecabcl  6556  fopwdom  7010  phplem4dom  7036  phpm  7040  phplem4on  7042  fidifsnen  7045  diffisn  7068  diffifi  7069  en2eqpr  7085  fisseneq  7112  suplub2ti  7184  difinfsn  7283  ctmlemr  7291  ctm  7292  ctssdclemn0  7293  ctssdc  7296  nninfninc  7306  nninfisol  7316  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  nninfwlpoimlemginf  7359  exmidontriimlem4  7422  exmidontriim  7423  cc3  7470  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  ltexnqq  7611  enq0tr  7637  addcmpblnq0  7646  mulcmpblnq0  7647  nnnq0lem1  7649  prssnqu  7683  prarloclemup  7698  nqprl  7754  nqpru  7755  mullocpr  7774  cauappcvgprlemladdfu  7857  cauappcvgprlemladdrl  7860  caucvgprlemm  7871  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlemlim  7884  caucvgprprlemml  7897  caucvgprprlemloc  7906  caucvgprprlemlim  7914  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  ltsrprg  7950  srpospr  7986  caucvgsrlemoffres  8003  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  axcaucvglemcau  8101  axsuploc  8235  cnegexlem3  8339  negeu  8353  add20  8637  rimul  8748  apreap  8750  cru  8765  apreim  8766  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  apti  8785  aptap  8813  mulap0  8817  prodgt0  9015  ltmul12a  9023  ledivdiv  9053  lediv12a  9057  supinfneg  9807  infsupneg  9808  qapne  9851  xaddf  10057  xaddval  10058  xleadd1a  10086  xleaddadd  10100  ixxss12  10119  ioodisj  10206  fznlem  10254  zsupcllemstep  10466  qtri3or  10477  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  addmodlteq  10637  seqf1og  10760  mulexpzap  10818  leexp1a  10833  expnbnd  10902  apexp1  10957  faclbnd  10980  hashxp  11066  zfz1iso  11081  swrdswrdlem  11257  cjap  11438  caucvgre  11513  cvg1nlemres  11517  resqrexlemglsq  11554  resqrexlemga  11555  sqrtsq  11576  ltabs  11619  abs3lem  11643  cau3lem  11646  maxleim  11737  rexico  11753  minmax  11762  xrmaxleim  11776  xrmaxiflemcl  11777  xrmaxiflemlub  11780  xrmaxiflemval  11782  xrmaxltsup  11790  xrmaxadd  11793  xrminmax  11797  xrbdtri  11808  climcau  11879  climrecvg1n  11880  sumeq2  11891  summodclem2  11914  divcnv  12029  prodeq2  12089  fprodsplitdc  12128  fprodconst  12152  dvdsle  12376  bitsfzo  12487  dvdsbnd  12498  bezoutlemmain  12540  bezoutlemzz  12544  bezoutlembi  12547  dfgcd3  12552  dvdsmulgcd  12567  nnmindc  12576  lcmcllem  12610  lcmgcdlem  12620  ncoprmgcdne1b  12632  isprm5  12685  pw2dvdslemn  12708  oddpwdclemxy  12712  pythagtriplem2  12810  pythagtrip  12827  pceu  12839  pc2dvds  12874  pcz  12876  pcadd  12884  pcfac  12894  exmidunben  13018  ctiunctlemfo  13031  unct  13034  prdsval  13327  sgrppropd  13467  sgrpidmndm  13474  mndpropd  13494  mhmeql  13546  isgrpinv  13608  dfgrp3mlem  13652  mhmmnd  13674  conjnmzb  13838  ghmcmn  13885  gsumfzconst  13899  isrng  13918  issrg  13949  isring  13984  dvdsrmul1  14087  tgrest  14864  cnpnei  14914  cnss1  14921  cncnp  14925  ismet2  15049  metequiv2  15191  metcnp  15207  metcnp2  15208  metcnpi3  15212  fsumcncntop  15262  elcncf2  15269  cncfmet  15287  suplociccreex  15319  dedekindicclemicc  15327  ivthinclemlr  15332  ivthinclemur  15334  cnplimclemr  15364  limccnpcntop  15370  limccoap  15373  dvmptfsum  15420  elply2  15430  plyrecj  15458  mersenne  15692  lgsval2lem  15710  lgsquad3  15784  usgr1eop  16064  usgr1vr  16067  pw1ndom3  16467  nninfalllem1  16488  nnnninfex  16502  sbthom  16508  apdiff  16530