Theorem 3simpa 1020

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

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

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 1006

This theorem is referenced by:  3simpb  1021  3simpc  1022  simp1  1023  simp2  1024  3adant3  1043  3adantl3  1181  3adantr3  1184  opprc  3883  oprcl  3886  opm  4326  funtpg  5381  ftpg  5837  ovig  6142  prltlu  7706  mullocpr  7790  lt2halves  9379  nn0n0n1ge2  9549  ixxssixx  10136  pfxsuffeqwrdeq  11278  pfxccatpfx1  11316  pfxccatpfx2  11317  sumtp  11974  dvdsmulcr  12381  dvds2add  12385  dvds2sub  12386  dvdstr  12388  dfgrp3me  13682  uhgrissubgr  16111  subgrprop3  16112  0uhgrsubgr  16115  wlkex  16175  wlkelwrd  16203  bj-peano4  16550