Theorem 3simpb 1155

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

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

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 1094

This theorem is referenced by:  3adantl2  1174  3adantr2  1177  fpropnf1  7218  cfcof  10194  axcclem  10377  enqeq  10855  leltletr  11235  ltleletr  11237  ixxssixx  13310  prodmolem2  15898  prodmo  15899  zprod  15900  muldvds1  16247  dvds2add  16257  dvds2sub  16258  dvdstr  16261  initoeu2lem2  17980  pospropd  18289  mndissubm  18773  csrgbinom  20211  smadiadetglem2  22662  ismbf3d  25646  mbfi1flimlem  25714  colinearalg  29004  frusgrnn0  29665  2wlkond  30030  2pthond  30035  2pthon3v  30036  umgr2adedgwlkonALT  30040  vdgn1frgrv2  30391  frgr2wwlkeqm  30426  bnj967  35134  bnj1110  35171  fineqvinfep  35313  subgrwlk  35367  cgr3permute3  36282  cgr3com  36288  brofs2  36312  bj-idreseq  37529  areacirclem4  38085  paddasslem14  40332  lhpexle1  40507  cdlemk19w  41471  ismrc  43157  iocinico  43664  gneispb  44582  fourierdlem113  46669  sigaras  47305  sigarms  47306  plusmod5ne  47821  gpgusgralem  48554  lincresunit3lem3  48972  lincresunit3  48979