Theorem simpllr 523

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 479	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  531  f1o2ndf1  6118  tfrlem1  6198  tfr1onlemaccex  6238  tfrcllemaccex  6251  frecabcl  6289  fopwdom  6723  phplem4dom  6749  phpm  6752  phplem4on  6754  fidifsnen  6757  diffisn  6780  diffifi  6781  en2eqpr  6794  fisseneq  6813  suplub2ti  6881  difinfsn  6978  ctmlemr  6986  ctm  6987  ctssdclemn0  6988  ctssdc  6991  enomnilem  7003  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  ltexnqq  7209  enq0tr  7235  addcmpblnq0  7244  mulcmpblnq0  7245  nnnq0lem1  7247  prssnqu  7281  prarloclemup  7296  nqprl  7352  nqpru  7353  mullocpr  7372  cauappcvgprlemladdfu  7455  cauappcvgprlemladdrl  7458  caucvgprlemm  7469  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlemlim  7482  caucvgprprlemml  7495  caucvgprprlemloc  7504  caucvgprprlemlim  7512  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  ltsrprg  7548  srpospr  7584  caucvgsrlemoffres  7601  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  axcaucvglemcau  7699  axsuploc  7830  cnegexlem3  7932  negeu  7946  add20  8229  rimul  8340  apreap  8342  cru  8357  apreim  8358  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  apti  8377  mulap0  8408  prodgt0  8603  ltmul12a  8611  ledivdiv  8641  lediv12a  8645  supinfneg  9383  infsupneg  9384  qapne  9424  xaddf  9620  xaddval  9621  xleadd1a  9649  xleaddadd  9663  ixxss12  9682  ioodisj  9769  fznlem  9814  qtri3or  10013  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  addmodlteq  10164  mulexpzap  10326  leexp1a  10341  expnbnd  10408  faclbnd  10480  hashxp  10565  zfz1iso  10577  cjap  10671  caucvgre  10746  cvg1nlemres  10750  resqrexlemglsq  10787  resqrexlemga  10788  sqrtsq  10809  ltabs  10852  abs3lem  10876  cau3lem  10879  maxleim  10970  rexico  10986  minmax  10994  xrmaxleim  11006  xrmaxiflemcl  11007  xrmaxiflemlub  11010  xrmaxiflemval  11012  xrmaxltsup  11020  xrmaxadd  11023  xrminmax  11027  xrbdtri  11038  climcau  11109  climrecvg1n  11110  sumeq2  11121  summodclem2  11144  divcnv  11259  prodeq2  11319  dvdsle  11531  zsupcllemstep  11627  dvdsbnd  11634  gcdsupex  11635  gcdsupcl  11636  bezoutlemmain  11675  bezoutlemzz  11679  bezoutlembi  11682  dfgcd3  11687  dvdsmulgcd  11702  lcmcllem  11737  lcmgcdlem  11747  ncoprmgcdne1b  11759  pw2dvdslemn  11832  oddpwdclemxy  11836  exmidunben  11928  ctiunctlemfo  11941  unct  11943  tgrest  12327  cnpnei  12377  cnss1  12384  cncnp  12388  ismet2  12512  metequiv2  12654  metcnp  12670  metcnp2  12671  metcnpi3  12675  fsumcncntop  12714  elcncf2  12719  cncfmet  12737  suplociccreex  12760  dedekindicclemicc  12768  ivthinclemlr  12773  ivthinclemur  12775  cnplimclemr  12796  limccnpcntop  12802  limccoap  12805  nninfalllem1  13192  sbthom  13210