Theorem 3simpa 935

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

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

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 921

This theorem is referenced by:  3simpb  936  3simpc  937  simp1  938  simp2  939  3adant3  958  3adantl3  1096  3adantr3  1099  opprc  3591  oprcl  3594  opm  3989  funtpg  4970  ftpg  5368  ovig  5642  prltlu  6677  mullocpr  6761  lt2halves  8266  nn0n0n1ge2  8418  ixxssixx  8925  dvdsmulcr  10225  dvds2add  10229  dvds2sub  10230  dvdstr  10232  bj-peano4  10750