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  4106  fnfi  7205  mapfi  7216  nninfisol  7426  swrdccatin1  11425  sumeq2  12052  zsumdc  12078  modfsummod  12152  prodeq2  12251  zproddc  12273  mulgval  13860  mplsubgfilemcl  14903  cncnp  15144  fsumcncntop  15481  dvmptfsum  15639  dvply2g  15680  logbgcd1irrap  15884  upgriswlkdc  16404  clwwlkccatlem  16444