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  4084  fnfi  7140  nninfisol  7337  swrdccatin1  11315  sumeq2  11942  zsumdc  11968  modfsummod  12042  prodeq2  12141  zproddc  12163  mulgval  13732  mplsubgfilemcl  14742  cncnp  14983  fsumcncntop  15320  dvmptfsum  15478  dvply2g  15519  logbgcd1irrap  15723  upgriswlkdc  16240  clwwlkccatlem  16280