Theorem 3simpa 940

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

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

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 926

This theorem is referenced by:  3simpb  941  3simpc  942  simp1  943  simp2  944  3adant3  963  3adantl3  1101  3adantr3  1104  opprc  3643  oprcl  3646  opm  4061  funtpg  5065  ftpg  5481  ovig  5766  prltlu  7046  mullocpr  7130  lt2halves  8651  nn0n0n1ge2  8817  ixxssixx  9320  sumtp  10808  dvdsmulcr  11104  dvds2add  11108  dvds2sub  11109  dvdstr  11111  bj-peano4  11850