Theorem 3simpb 1149

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 1131	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adantl2  1168  3adantr2  1171  fpropnf1  7213  cfcof  10184  axcclem  10367  enqeq  10845  leltletr  11224  ltleletr  11226  ixxssixx  13275  prodmolem2  15858  prodmo  15859  zprod  15860  muldvds1  16207  dvds2add  16217  dvds2sub  16218  dvdstr  16221  initoeu2lem2  17939  pospropd  18248  mndissubm  18732  csrgbinom  20167  smadiadetglem2  22616  ismbf3d  25611  mbfi1flimlem  25679  colinearalg  28983  frusgrnn0  29645  2wlkond  30010  2pthond  30015  2pthon3v  30016  umgr2adedgwlkonALT  30020  vdgn1frgrv2  30371  frgr2wwlkeqm  30406  bnj967  35101  bnj1110  35138  fineqvinfep  35281  subgrwlk  35326  cgr3permute3  36241  cgr3com  36247  brofs2  36271  bj-idreseq  37367  areacirclem4  37912  paddasslem14  40093  lhpexle1  40268  cdlemk19w  41232  ismrc  42943  iocinico  43454  gneispb  44372  fourierdlem113  46463  sigaras  47099  sigarms  47100  plusmod5ne  47591  gpgusgralem  48302  lincresunit3lem3  48720  lincresunit3  48727