Theorem 3simpa 901

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

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

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

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3simpb  902  3simpc  903  simp1  904  simp2  905  3adant3  924  3adantl3  1062  3adantr3  1065  opprc  3570  oprcl  3573  opm  3971  funtpg  4950  ftpg  5347  ovig  5622  prltlu  6585  mullocpr  6669  lt2halves  8160  nn0n0n1ge2  8311  ixxssixx  8771  bj-peano4  10080