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  3881  oprcl  3884  opm  4324  funtpg  5378  ftpg  5833  ovig  6138  prltlu  7697  mullocpr  7781  lt2halves  9370  nn0n0n1ge2  9540  ixxssixx  10127  pfxsuffeqwrdeq  11269  pfxccatpfx1  11307  pfxccatpfx2  11308  sumtp  11965  dvdsmulcr  12372  dvds2add  12376  dvds2sub  12377  dvdstr  12379  dfgrp3me  13673  wlkex  16122  wlkelwrd  16150  bj-peano4  16486