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  3904  oprcl  3907  opm  4350  funtpg  5407  ftpg  5868  ovig  6175  prltlu  7802  mullocpr  7886  lt2halves  9474  nn0n0n1ge2  9648  ixxssixx  10235  pfxsuffeqwrdeq  11390  pfxccatpfx1  11428  pfxccatpfx2  11429  sumtp  12100  dvdsmulcr  12507  dvds2add  12511  dvds2sub  12512  dvdstr  12514  dfgrp3me  13813  uhgrissubgr  16256  subgrprop3  16257  0uhgrsubgr  16260  wlkex  16320  wlkelwrd  16348  bj-peano4  16725