Theorem simpllr 502

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 473	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp-4r  510  f1o2ndf1  6031  tfrlem1  6111  tfr1onlemaccex  6151  tfrcllemaccex  6164  frecabcl  6202  fopwdom  6632  phplem4dom  6658  phpm  6661  phplem4on  6663  fidifsnen  6666  diffisn  6689  diffifi  6690  en2eqpr  6703  fisseneq  6722  suplub2ti  6776  ctmlemr  6870  ctm  6871  enomnilem  6881  addcmpblnq  7023  mulcmpblnq  7024  ordpipqqs  7030  ltexnqq  7064  enq0tr  7090  addcmpblnq0  7099  mulcmpblnq0  7100  nnnq0lem1  7102  prssnqu  7136  prarloclemup  7151  nqprl  7207  nqpru  7208  mullocpr  7227  cauappcvgprlemladdfu  7310  cauappcvgprlemladdrl  7313  caucvgprlemm  7324  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlemlim  7337  caucvgprprlemml  7350  caucvgprprlemloc  7359  caucvgprprlemlim  7367  addcmpblnr  7382  mulcmpblnrlemg  7383  mulcmpblnr  7384  ltsrprg  7390  srpospr  7425  caucvgsrlemoffres  7442  axcaucvglemcau  7530  cnegexlem3  7756  negeu  7770  add20  8049  rimul  8159  apreap  8161  cru  8176  apreim  8177  apsym  8180  apcotr  8181  apadd1  8182  apneg  8185  mulext1  8186  apti  8196  mulap0  8220  prodgt0  8410  ltmul12a  8418  ledivdiv  8448  lediv12a  8452  supinfneg  9182  infsupneg  9183  qapne  9223  xaddf  9410  xaddval  9411  xleadd1a  9439  xleaddadd  9453  ixxss12  9472  ioodisj  9559  fznlem  9604  qtri3or  9803  exbtwnzlemstep  9808  rebtwn2zlemstep  9813  addmodlteq  9954  mulexpzap  10110  leexp1a  10125  expnbnd  10192  faclbnd  10264  hashxp  10349  zfz1iso  10361  cjap  10455  caucvgre  10529  cvg1nlemres  10533  resqrexlemglsq  10570  resqrexlemga  10571  sqrtsq  10592  ltabs  10635  abs3lem  10659  cau3lem  10662  maxleim  10753  rexico  10769  minmax  10776  xrmaxleim  10787  xrmaxiflemcl  10788  xrmaxiflemlub  10791  xrmaxiflemval  10793  xrmaxltsup  10801  xrmaxadd  10804  xrminmax  10808  xrbdtri  10819  climcau  10890  climrecvg1n  10891  sumeq2  10902  summodclem2  10925  divcnv  11040  dvdsle  11272  zsupcllemstep  11368  dvdsbnd  11375  gcdsupex  11376  gcdsupcl  11377  bezoutlemmain  11414  bezoutlemzz  11418  bezoutlembi  11421  dfgcd3  11426  dvdsmulgcd  11441  lcmcllem  11476  lcmgcdlem  11486  ncoprmgcdne1b  11498  pw2dvdslemn  11570  oddpwdclemxy  11574  tgrest  12021  cnpnei  12070  cnss1  12077  cncnp  12081  ismet2  12140  metequiv2  12282  metcnp  12294  metcnp2  12295  metcnpi3  12299  elcncf2  12329  cncfmet  12347  nninfalllem1  12613