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  3877  oprcl  3880  opm  4319  funtpg  5371  ftpg  5822  ovig  6125  prltlu  7670  mullocpr  7754  lt2halves  9343  nn0n0n1ge2  9513  ixxssixx  10094  pfxsuffeqwrdeq  11225  pfxccatpfx1  11263  pfxccatpfx2  11264  sumtp  11920  dvdsmulcr  12327  dvds2add  12331  dvds2sub  12332  dvdstr  12334  dfgrp3me  13628  bj-peano4  16276