Theorem 3simpa 997

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

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

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 983

This theorem is referenced by:  3simpb  998  3simpc  999  simp1  1000  simp2  1001  3adant3  1020  3adantl3  1158  3adantr3  1161  opprc  3846  oprcl  3849  opm  4286  funtpg  5334  ftpg  5781  ovig  6080  prltlu  7620  mullocpr  7704  lt2halves  9293  nn0n0n1ge2  9463  ixxssixx  10044  pfxsuffeqwrdeq  11174  sumtp  11800  dvdsmulcr  12207  dvds2add  12211  dvds2sub  12212  dvdstr  12214  dfgrp3me  13507  bj-peano4  16029