Theorem 3simpa 979

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3simpa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Proof of Theorem 3simpa

Step	Hyp	Ref	Expression
1		df-3an 965	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2	1	simplbi 272	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3simpb  980  3simpc  981  simp1  982  simp2  983  3adant3  1002  3adantl3  1140  3adantr3  1143  opprc  3734  oprcl  3737  opm  4164  funtpg  5182  ftpg  5612  ovig  5900  prltlu  7319  mullocpr  7403  lt2halves  8979  nn0n0n1ge2  9145  ixxssixx  9715  sumtp  11215  dvdsmulcr  11559  dvds2add  11563  dvds2sub  11564  dvdstr  11566  bj-peano4  13324