Theorem simp-4l 541

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 533	. 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  543  disjiun  4077  fnfi  7099  nninfisol  7296  swrdccatin1  11252  sumeq2  11865  zsumdc  11890  modfsummod  11964  prodeq2  12063  zproddc  12085  mulgval  13654  mplsubgfilemcl  14657  cncnp  14898  fsumcncntop  15235  dvmptfsum  15393  dvply2g  15434  logbgcd1irrap  15638