Theorem 3simpa 978

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

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

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 964

This theorem is referenced by:  3simpb  979  3simpc  980  simp1  981  simp2  982  3adant3  1001  3adantl3  1139  3adantr3  1142  opprc  3726  oprcl  3729  opm  4156  funtpg  5174  ftpg  5604  ovig  5892  prltlu  7295  mullocpr  7379  lt2halves  8955  nn0n0n1ge2  9121  ixxssixx  9685  sumtp  11183  dvdsmulcr  11523  dvds2add  11527  dvds2sub  11528  dvdstr  11530  bj-peano4  13153