Theorem simp-4r 544

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		simpllr 536	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 276	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-5r  546  fimax2gtri  7134  finexdc  7135  dcfi  7223  difinfsn  7342  nnnninfeq2  7371  nninfisol  7375  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  suplocexprlemru  7982  suplocsrlemb  8069  suplocsrlem  8071  aptap  8873  supinfneg  9872  infsupneg  9873  xaddf  10122  xaddval  10123  nn0ltexp2  11015  hashunlem  11111  swrdccatin1  11353  reuccatpfxs1  11375  xrmaxiflemcl  11866  xrmaxiflemlub  11869  xrmaxltsup  11879  sumeq2  11980  fsumconst  12076  prodeq2  12179  fprodconst  12242  nninfctlemfo  12672  prdsval  13417  sgrpidmndm  13564  mhmmnd  13764  ghmcmn  13975  issrg  14040  cncnp  15021  neitx  15059  dedekindeulemlu  15412  suplociccreex  15415  dedekindicclemlu  15421  cnplimclemr  15460  limccnp2cntop  15468  logbgcd1irrap  15761  lgsval  15800  usgr1vr  16166  pw1ndom3  16687