Theorem 3simpa 1021

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

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

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 1007

This theorem is referenced by:  3simpb  1022  3simpc  1023  simp1  1024  simp2  1025  3adant3  1044  3adantl3  1182  3adantr3  1185  opprc  3888  oprcl  3891  opm  4332  funtpg  5388  ftpg  5846  ovig  6153  prltlu  7750  mullocpr  7834  lt2halves  9422  nn0n0n1ge2  9594  ixxssixx  10181  pfxsuffeqwrdeq  11328  pfxccatpfx1  11366  pfxccatpfx2  11367  sumtp  12038  dvdsmulcr  12445  dvds2add  12449  dvds2sub  12450  dvdstr  12452  dfgrp3me  13746  uhgrissubgr  16185  subgrprop3  16186  0uhgrsubgr  16189  wlkex  16249  wlkelwrd  16277  bj-peano4  16654