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  6468  tfrlem1  6583  tfr1onlemaccex  6623  tfrcllemaccex  6636  frecabcl  6674  fopwdom  7141  phplem4dom  7168  phpm  7172  phplem4on  7174  fidifsnen  7177  diffisn  7202  diffifi  7203  en2eqpr  7219  fisseneq  7247  suplub2ti  7348  difinfsn  7447  ctmlemr  7455  ctm  7456  ctssdclemn0  7457  ctssdc  7460  nninfninc  7470  nninfisol  7480  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  nninfwlpoimlemginf  7523  exmidontriimlem4  7587  exmidontriim  7588  cc3  7641  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  ltexnqq  7782  enq0tr  7808  addcmpblnq0  7817  mulcmpblnq0  7818  nnnq0lem1  7820  prssnqu  7854  prarloclemup  7869  nqprl  7925  nqpru  7926  mullocpr  7945  cauappcvgprlemladdfu  8028  cauappcvgprlemladdrl  8031  caucvgprlemm  8042  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprlemlim  8055  caucvgprprlemml  8068  caucvgprprlemloc  8077  caucvgprprlemlim  8085  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  ltsrprg  8121  srpospr  8157  caucvgsrlemoffres  8174  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  axcaucvglemcau  8272  axsuploc  8405  cnegexlem3  8511  negeu  8525  add20  8810  rimul  8922  apreap  8924  cru  8939  apreim  8940  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  apti  8959  aptap  8987  mulap0  8991  prodgt0  9191  ltmul12a  9199  ledivdiv  9229  lediv12a  9233  supinfneg  10012  infsupneg  10013  qapne  10056  irraddap  10064  xaddf  10264  xaddval  10265  xleadd1a  10293  xleaddadd  10307  ixxss12  10326  ioodisj  10413  fznlem  10463  zsupcllemstep  10680  qtri3or  10693  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  addmodlteq  10857  seqf1og  10980  mulexpzap  11038  leexp1a  11053  expnbnd  11123  apexp1  11179  faclbnd  11202  hashxp  11290  sshashneg  11304  hashf1lem2  11309  zfz1iso  11316  swrdswrdlem  11499  cjap  11695  caucvgre  11770  cvg1nlemres  11774  resqrexlemglsq  11811  resqrexlemga  11812  sqrtsq  11833  ltabs  11877  abs3lem  11901  cau3lem  11904  maxleim  11995  rexico  12011  fiidxsupcl  12019  minmax  12021  xrmaxleim  12036  xrmaxiflemcl  12037  xrmaxiflemlub  12040  xrmaxiflemval  12042  xrmaxltsup  12050  xrmaxadd  12053  xrminmax  12057  xrbdtri  12068  climcau  12139  climrecvg1n  12140  sumeq2  12151  summodclem2  12175  divcnv  12290  prodeq2  12350  fprodsplitdc  12389  fprodconst  12413  dvdsle  12637  bitsfzo  12748  dvdsbnd  12759  bezoutlemmain  12801  bezoutlemzz  12805  bezoutlembi  12808  dfgcd3  12813  dvdsmulgcd  12828  nnmindc  12837  lcmcllem  12871  lcmgcdlem  12881  ncoprmgcdne1b  12893  isprm5  12947  pwbdvdslemn  12970  nnmaxpwlemparts  12978  pythagtriplem2  13075  pythagtrip  13092  pceu  13104  pc2dvds  13139  pcz  13141  pcadd  13149  pcfac  13159  exmidunben  13376  ctiunctlemfo  13389  unct  13392  sgrppropd  13788  sgrpidmndm  13793  mndpropd  13813  mhmeql  13859  isgrpinv  13919  dfgrp3mlem  13963  mhmmnd  13979  conjnmzb  14143  resscntz  14167  ghmcmn  14222  gzsumconst  14234  prdsval  14281  isrng  14341  issrg  14377  isring  14412  dvdsrmul1  14519  aprlring  14710  issubassa2  15145  tgrest  15407  cnpnei  15457  cnss1  15464  cncnp  15468  ismet2  15592  metequiv2  15734  metcnp  15750  metcnp2  15751  metcnpi3  15755  fsumcncntop  15805  elcncf2  15812  cncfmet  15830  suplociccreex  15862  dedekindicclemicc  15870  ivthinclemlr  15875  ivthinclemur  15877  cnplimclemr  15907  limccnpcntop  15913  limccoap  15916  dvmptfsum  15963  elply2  15973  plyrecj  16001  logdivlt  16136  zprmlogbap  16230  mersenne  16309  lgsval2lem  16346  lgsquad3  16420  usgr1eop  16703  usgr1vr  16706  pw1ndom3  17237  nninfalllem1  17269  nnnninfex  17283  sbthom  17289  apdiff  17316