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 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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-5l  549  disjiun  4123  fnfi  7244  mapfi  7255  nninfisol  7467  swrdccatin1  11480  sumeq2  12108  zsumdc  12134  modfsummod  12208  prodeq2  12307  zproddc  12329  mulgval  13908  mplsubgfilemcl  15073  cncnp  15314  fsumcncntop  15651  dvmptfsum  15809  dvply2g  15850  logbgcd1irrap  16055  upgriswlkdc  16584  clwwlkccatlem  16624