Theorem 3simpa 936

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 922	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2	1	simplbi 268	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3simpb  937  3simpc  938  simp1  939  simp2  940  3adant3  959  3adantl3  1097  3adantr3  1100  opprc  3612  oprcl  3615  opm  4018  funtpg  5002  ftpg  5401  ovig  5675  prltlu  6816  mullocpr  6900  lt2halves  8410  nn0n0n1ge2  8576  ixxssixx  9078  dvdsmulcr  10458  dvds2add  10462  dvds2sub  10463  dvdstr  10465  bj-peano4  11042