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  6380  tfrlem1  6460  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecabcl  6551  fopwdom  7005  phplem4dom  7031  phpm  7035  phplem4on  7037  fidifsnen  7040  diffisn  7063  diffifi  7064  en2eqpr  7077  fisseneq  7104  suplub2ti  7176  difinfsn  7275  ctmlemr  7283  ctm  7284  ctssdclemn0  7285  ctssdc  7288  nninfninc  7298  nninfisol  7308  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  nninfwlpoimlemginf  7351  exmidontriimlem4  7414  exmidontriim  7415  cc3  7462  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  ltexnqq  7603  enq0tr  7629  addcmpblnq0  7638  mulcmpblnq0  7639  nnnq0lem1  7641  prssnqu  7675  prarloclemup  7690  nqprl  7746  nqpru  7747  mullocpr  7766  cauappcvgprlemladdfu  7849  cauappcvgprlemladdrl  7852  caucvgprlemm  7863  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprlemlim  7876  caucvgprprlemml  7889  caucvgprprlemloc  7898  caucvgprprlemlim  7906  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  ltsrprg  7942  srpospr  7978  caucvgsrlemoffres  7995  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  axcaucvglemcau  8093  axsuploc  8227  cnegexlem3  8331  negeu  8345  add20  8629  rimul  8740  apreap  8742  cru  8757  apreim  8758  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  apti  8777  aptap  8805  mulap0  8809  prodgt0  9007  ltmul12a  9015  ledivdiv  9045  lediv12a  9049  supinfneg  9798  infsupneg  9799  qapne  9842  xaddf  10048  xaddval  10049  xleadd1a  10077  xleaddadd  10091  ixxss12  10110  ioodisj  10197  fznlem  10245  zsupcllemstep  10457  qtri3or  10468  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  addmodlteq  10628  seqf1og  10751  mulexpzap  10809  leexp1a  10824  expnbnd  10893  apexp1  10948  faclbnd  10971  hashxp  11056  zfz1iso  11071  swrdswrdlem  11244  cjap  11425  caucvgre  11500  cvg1nlemres  11504  resqrexlemglsq  11541  resqrexlemga  11542  sqrtsq  11563  ltabs  11606  abs3lem  11630  cau3lem  11633  maxleim  11724  rexico  11740  minmax  11749  xrmaxleim  11763  xrmaxiflemcl  11764  xrmaxiflemlub  11767  xrmaxiflemval  11769  xrmaxltsup  11777  xrmaxadd  11780  xrminmax  11784  xrbdtri  11795  climcau  11866  climrecvg1n  11867  sumeq2  11878  summodclem2  11901  divcnv  12016  prodeq2  12076  fprodsplitdc  12115  fprodconst  12139  dvdsle  12363  bitsfzo  12474  dvdsbnd  12485  bezoutlemmain  12527  bezoutlemzz  12531  bezoutlembi  12534  dfgcd3  12539  dvdsmulgcd  12554  nnmindc  12563  lcmcllem  12597  lcmgcdlem  12607  ncoprmgcdne1b  12619  isprm5  12672  pw2dvdslemn  12695  oddpwdclemxy  12699  pythagtriplem2  12797  pythagtrip  12814  pceu  12826  pc2dvds  12861  pcz  12863  pcadd  12871  pcfac  12881  exmidunben  13005  ctiunctlemfo  13018  unct  13021  prdsval  13314  sgrppropd  13454  sgrpidmndm  13461  mndpropd  13481  mhmeql  13533  isgrpinv  13595  dfgrp3mlem  13639  mhmmnd  13661  conjnmzb  13825  ghmcmn  13872  gsumfzconst  13886  isrng  13905  issrg  13936  isring  13971  dvdsrmul1  14074  tgrest  14851  cnpnei  14901  cnss1  14908  cncnp  14912  ismet2  15036  metequiv2  15178  metcnp  15194  metcnp2  15195  metcnpi3  15199  fsumcncntop  15249  elcncf2  15256  cncfmet  15274  suplociccreex  15306  dedekindicclemicc  15314  ivthinclemlr  15319  ivthinclemur  15321  cnplimclemr  15351  limccnpcntop  15357  limccoap  15360  dvmptfsum  15407  elply2  15417  plyrecj  15445  mersenne  15679  lgsval2lem  15697  lgsquad3  15771  pw1ndom3  16383  nninfalllem1  16404  nnnninfex  16418  sbthom  16424  apdiff  16446