Theorem 3simpa 996

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

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

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 982

This theorem is referenced by:  3simpb  997  3simpc  998  simp1  999  simp2  1000  3adant3  1019  3adantl3  1157  3adantr3  1160  opprc  3839  oprcl  3842  opm  4277  funtpg  5319  ftpg  5758  ovig  6057  prltlu  7582  mullocpr  7666  lt2halves  9255  nn0n0n1ge2  9425  ixxssixx  10006  sumtp  11644  dvdsmulcr  12051  dvds2add  12055  dvds2sub  12056  dvdstr  12058  dfgrp3me  13350  bj-peano4  15755