Theorem simp-4r 531

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 523	. 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  533  fimax2gtri  6795  finexdc  6796  difinfsn  6985  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  suplocexprlemru  7527  suplocsrlemb  7614  suplocsrlem  7616  supinfneg  9390  infsupneg  9391  xaddf  9627  xaddval  9628  hashunlem  10550  xrmaxiflemcl  11014  xrmaxiflemlub  11017  xrmaxltsup  11027  sumeq2  11128  fsumconst  11223  prodeq2  11326  cncnp  12399  neitx  12437  dedekindeulemlu  12768  suplociccreex  12771  dedekindicclemlu  12777  cnplimclemr  12807  limccnp2cntop  12815