Theorem 3simpa 1020

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

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

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 1006

This theorem is referenced by:  3simpb  1021  3simpc  1022  simp1  1023  simp2  1024  3adant3  1043  3adantl3  1181  3adantr3  1184  opprc  3883  oprcl  3886  opm  4326  funtpg  5381  ftpg  5838  ovig  6143  prltlu  7707  mullocpr  7791  lt2halves  9380  nn0n0n1ge2  9550  ixxssixx  10137  pfxsuffeqwrdeq  11283  pfxccatpfx1  11321  pfxccatpfx2  11322  sumtp  11980  dvdsmulcr  12387  dvds2add  12391  dvds2sub  12392  dvdstr  12394  dfgrp3me  13688  uhgrissubgr  16118  subgrprop3  16119  0uhgrsubgr  16122  wlkex  16182  wlkelwrd  16210  bj-peano4  16576