Theorem simp-4l 543

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 535	. 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  545  disjiun  4109  fnfi  7216  mapfi  7227  nninfisol  7437  swrdccatin1  11445  sumeq2  12072  zsumdc  12098  modfsummod  12172  prodeq2  12271  zproddc  12293  mulgval  13878  mplsubgfilemcl  14983  cncnp  15224  fsumcncntop  15561  dvmptfsum  15719  dvply2g  15760  logbgcd1irrap  15964  upgriswlkdc  16484  clwwlkccatlem  16524