Theorem 3simpb 1142

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Assertion

Ref	Expression
3simpb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Proof of Theorem 3simpb

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒))
2	1	3adant2 1124	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082

This theorem is referenced by:  3adantl2  1160  3adantr2  1163  fpropnf1  6893  cfcof  9545  axcclem  9728  enqeq  10205  ltleletr  10582  ixxssixx  12602  prodmolem2  15122  prodmo  15123  zprod  15124  muldvds1  15467  dvds2add  15476  dvds2sub  15477  dvdstr  15479  initoeu2lem2  17104  pospropd  17573  csrgbinom  18986  smadiadetglem2  20965  ismbf3d  23938  mbfi1flimlem  24006  colinearalg  26379  frusgrnn0  27036  2wlkond  27398  2pthond  27403  2pthon3v  27404  umgr2adedgwlkonALT  27408  vdgn1frgrv2  27759  frgr2wwlkeqm  27794  bnj967  31825  bnj1110  31860  subgrwlk  31981  cgr3permute3  33111  cgr3com  33117  brofs2  33141  areacirclem4  34529  paddasslem14  36513  lhpexle1  36688  cdlemk19w  37652  ismrc  38796  iocinico  39316  gneispb  39979  fourierdlem113  42060  sigaras  42668  sigarms  42669  leltletr  43023  lincresunit3lem3  44023  lincresunit3  44030