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  4103  fnfi  7202  mapfi  7213  nninfisol  7423  swrdccatin1  11410  sumeq2  12037  zsumdc  12063  modfsummod  12137  prodeq2  12236  zproddc  12258  mulgval  13828  mplsubgfilemcl  14841  cncnp  15082  fsumcncntop  15419  dvmptfsum  15577  dvply2g  15618  logbgcd1irrap  15822  upgriswlkdc  16342  clwwlkccatlem  16382