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  4078  fnfi  7111  nninfisol  7308  swrdccatin1  11265  sumeq2  11878  zsumdc  11903  modfsummod  11977  prodeq2  12076  zproddc  12098  mulgval  13667  mplsubgfilemcl  14671  cncnp  14912  fsumcncntop  15249  dvmptfsum  15407  dvply2g  15448  logbgcd1irrap  15652  upgriswlkdc  16081