Theorem 3simpa 1025

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3simpb  1026  3simpc  1027  simp1  1028  simp2  1029  3adant3  1048  3adantl3  1186  3adantr3  1189  opprc  3925  oprcl  3928  opm  4376  funtpg  5435  ftpg  5902  ovig  6213  prltlu  7860  mullocpr  7944  lt2halves  9552  nn0n0n1ge2  9724  ixxssixx  10320  pfxsuffeqwrdeq  11491  pfxccatpfx1  11529  pfxccatpfx2  11530  sumtp  12205  dvdsmulcr  12612  dvds2add  12616  dvds2sub  12617  dvdstr  12619  dfgrp3me  13963  uhgrissubgr  16724  subgrprop3  16725  0uhgrsubgr  16728  wlkex  16788  wlkelwrd  16816  bj-peano4  17203