Theorem simp-4r 532

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 524	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 274	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-5r  534  fimax2gtri  6803  finexdc  6804  difinfsn  6993  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  suplocexprlemru  7551  suplocsrlemb  7638  suplocsrlem  7640  supinfneg  9417  infsupneg  9418  xaddf  9657  xaddval  9658  hashunlem  10582  xrmaxiflemcl  11046  xrmaxiflemlub  11049  xrmaxltsup  11059  sumeq2  11160  fsumconst  11255  prodeq2  11358  cncnp  12438  neitx  12476  dedekindeulemlu  12807  suplociccreex  12810  dedekindicclemlu  12816  cnplimclemr  12846  limccnp2cntop  12854  logbgcd1irrap  13095