Theorem 3simpa 1018

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

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

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 1004

This theorem is referenced by:  3simpb  1019  3simpc  1020  simp1  1021  simp2  1022  3adant3  1041  3adantl3  1179  3adantr3  1182  opprc  3878  oprcl  3881  opm  4320  funtpg  5372  ftpg  5827  ovig  6132  prltlu  7685  mullocpr  7769  lt2halves  9358  nn0n0n1ge2  9528  ixxssixx  10110  pfxsuffeqwrdeq  11245  pfxccatpfx1  11283  pfxccatpfx2  11284  sumtp  11940  dvdsmulcr  12347  dvds2add  12351  dvds2sub  12352  dvdstr  12354  dfgrp3me  13648  wlkex  16066  wlkelwrd  16094  bj-peano4  16373