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  7474  swrdccatin1  11513  sumeq2  12144  zsumdc  12170  modfsummod  12244  prodeq2  12343  zproddc  12365  mulgval  13978  mplsubgfilemcl  15181  cncnp  15422  fsumcncntop  15759  dvmptfsum  15917  dvply2g  15958  logbgcd1irrap  16172  upgriswlkdc  16772  clwwlkccatlem  16812