Theorem 3simpa 994

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

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

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 980

This theorem is referenced by:  3simpb  995  3simpc  996  simp1  997  simp2  998  3adant3  1017  3adantl3  1155  3adantr3  1158  opprc  3801  oprcl  3804  opm  4236  funtpg  5269  ftpg  5702  ovig  5998  prltlu  7488  mullocpr  7572  lt2halves  9156  nn0n0n1ge2  9325  ixxssixx  9904  sumtp  11424  dvdsmulcr  11830  dvds2add  11834  dvds2sub  11835  dvdstr  11837  dfgrp3me  12975  bj-peano4  14792