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  3762  oprcl  3765  opm  4194  funtpg  5220  ftpg  5650  ovig  5939  prltlu  7401  mullocpr  7485  lt2halves  9062  nn0n0n1ge2  9228  ixxssixx  9799  sumtp  11304  dvdsmulcr  11709  dvds2add  11713  dvds2sub  11714  dvdstr  11716  bj-peano4  13501