Theorem 3simpa 996

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3simpb  997  3simpc  998  simp1  999  simp2  1000  3adant3  1019  3adantl3  1157  3adantr3  1160  opprc  3829  oprcl  3832  opm  4267  funtpg  5309  ftpg  5746  ovig  6044  prltlu  7554  mullocpr  7638  lt2halves  9227  nn0n0n1ge2  9396  ixxssixx  9977  sumtp  11579  dvdsmulcr  11986  dvds2add  11990  dvds2sub  11991  dvdstr  11993  dfgrp3me  13232  bj-peano4  15601