Theorem simp-4l 547

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

Assertion

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

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		simplll 539	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	adantr 276	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-5l  549  disjiun  4125  fnfi  7250  mapfi  7261  nninfisol  7473  swrdccatin1  11499  sumeq2  12127  zsumdc  12153  modfsummod  12227  prodeq2  12326  zproddc  12348  mulgval  13927  mplsubgfilemcl  15092  cncnp  15333  fsumcncntop  15670  dvmptfsum  15828  dvply2g  15869  logbgcd1irrap  16078  upgriswlkdc  16613  clwwlkccatlem  16653