Theorem 3simpa 912

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

Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896

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

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  3simpb  913  3simpc  914  simp1  915  simp2  916  3adant3  935  3adantl3  1073  3adantr3  1076  opprc  3597  oprcl  3600  opm  3998  funtpg  4977  ftpg  5374  ovig  5649  prltlu  6642  mullocpr  6726  lt2halves  8216  nn0n0n1ge2  8368  ixxssixx  8871  dvdsmulcr  10136  dvds2add  10140  dvds2sub  10141  dvdstr  10143  bj-peano4  10446