Theorem simpllr 524

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 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 480	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4r  532  f1o2ndf1  6196  tfrlem1  6276  tfr1onlemaccex  6316  tfrcllemaccex  6329  frecabcl  6367  fopwdom  6802  phplem4dom  6828  phpm  6831  phplem4on  6833  fidifsnen  6836  diffisn  6859  diffifi  6860  en2eqpr  6873  fisseneq  6897  suplub2ti  6966  difinfsn  7065  ctmlemr  7073  ctm  7074  ctssdclemn0  7075  ctssdc  7078  nninfisol  7097  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  exmidontriimlem4  7180  exmidontriim  7181  cc3  7209  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  ltexnqq  7349  enq0tr  7375  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  prssnqu  7421  prarloclemup  7436  nqprl  7492  nqpru  7493  mullocpr  7512  cauappcvgprlemladdfu  7595  cauappcvgprlemladdrl  7598  caucvgprlemm  7609  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlemlim  7622  caucvgprprlemml  7635  caucvgprprlemloc  7644  caucvgprprlemlim  7652  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  ltsrprg  7688  srpospr  7724  caucvgsrlemoffres  7741  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axcaucvglemcau  7839  axsuploc  7971  cnegexlem3  8075  negeu  8089  add20  8372  rimul  8483  apreap  8485  cru  8500  apreim  8501  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  apti  8520  mulap0  8551  prodgt0  8747  ltmul12a  8755  ledivdiv  8785  lediv12a  8789  supinfneg  9533  infsupneg  9534  qapne  9577  xaddf  9780  xaddval  9781  xleadd1a  9809  xleaddadd  9823  ixxss12  9842  ioodisj  9929  fznlem  9976  qtri3or  10178  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  addmodlteq  10333  mulexpzap  10495  leexp1a  10510  expnbnd  10578  apexp1  10631  faclbnd  10654  hashxp  10739  zfz1iso  10754  cjap  10848  caucvgre  10923  cvg1nlemres  10927  resqrexlemglsq  10964  resqrexlemga  10965  sqrtsq  10986  ltabs  11029  abs3lem  11053  cau3lem  11056  maxleim  11147  rexico  11163  minmax  11171  xrmaxleim  11185  xrmaxiflemcl  11186  xrmaxiflemlub  11189  xrmaxiflemval  11191  xrmaxltsup  11199  xrmaxadd  11202  xrminmax  11206  xrbdtri  11217  climcau  11288  climrecvg1n  11289  sumeq2  11300  summodclem2  11323  divcnv  11438  prodeq2  11498  fprodsplitdc  11537  fprodconst  11561  dvdsle  11782  zsupcllemstep  11878  dvdsbnd  11889  gcdsupex  11890  gcdsupcl  11891  bezoutlemmain  11931  bezoutlemzz  11935  bezoutlembi  11938  dfgcd3  11943  dvdsmulgcd  11958  nnmindc  11967  lcmcllem  11999  lcmgcdlem  12009  ncoprmgcdne1b  12021  isprm5  12074  pw2dvdslemn  12097  oddpwdclemxy  12101  pythagtriplem2  12198  pythagtrip  12215  pceu  12227  pc2dvds  12261  pcz  12263  pcadd  12271  pcfac  12280  exmidunben  12359  ctiunctlemfo  12372  unct  12375  tgrest  12809  cnpnei  12859  cnss1  12866  cncnp  12870  ismet2  12994  metequiv2  13136  metcnp  13152  metcnp2  13153  metcnpi3  13157  fsumcncntop  13196  elcncf2  13201  cncfmet  13219  suplociccreex  13242  dedekindicclemicc  13250  ivthinclemlr  13255  ivthinclemur  13257  cnplimclemr  13278  limccnpcntop  13284  limccoap  13287  lgsval2lem  13551  nninfalllem1  13888  sbthom  13905  apdiff  13927