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  7209  cfcof  10174  axcclem  10357  enqeq  10834  leltletr  11213  ltleletr  11215  ixxssixx  13263  prodmolem2  15846  prodmo  15847  zprod  15848  muldvds1  16195  dvds2add  16205  dvds2sub  16206  dvdstr  16209  initoeu2lem2  17926  pospropd  18235  mndissubm  18719  csrgbinom  20154  smadiadetglem2  22590  ismbf3d  25585  mbfi1flimlem  25653  colinearalg  28892  frusgrnn0  29554  2wlkond  29919  2pthond  29924  2pthon3v  29925  umgr2adedgwlkonALT  29929  vdgn1frgrv2  30280  frgr2wwlkeqm  30315  bnj967  34980  bnj1110  35017  subgrwlk  35199  cgr3permute3  36114  cgr3com  36120  brofs2  36144  bj-idreseq  37229  areacirclem4  37774  paddasslem14  39955  lhpexle1  40130  cdlemk19w  41094  ismrc  42821  iocinico  43332  gneispb  44251  fourierdlem113  46344  sigaras  46980  sigarms  46981  plusmod5ne  47472  gpgusgralem  48183  lincresunit3lem3  48602  lincresunit3  48609