Theorem 3simpb 1167

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 23	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ 𝜒))
2	1	3adant2 1149	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl2  1186  3adantr2  1189  fpropnf1  7269  cfcof  10345  axcclem  10528  enqeq  11012  leltletr  11394  ltleletr  11396  ixxssixx  13483  prodmolem2  16095  prodmo  16096  zprod  16097  muldvds1  16443  dvds2add  16453  dvds2sub  16454  dvdstr  16457  initoeu2lem2  18183  pospropd  18492  mndissubm  18995  csrgbinom  20451  smadiadetglem2  22980  ismbf3d  25968  mbfi1flimlem  26036  colinearalg  29481  frusgrnn0  30145  subgrwlk  30262  2wlkond  30519  2pthond  30524  2pthon3v  30525  umgr2adedgwlkonALT  30529  vdgn1frgrv2  30890  frgr2wwlkeqm  30925  bnj967  35568  bnj1110  35605  fineqvinfep  35776  cgr3permute3  36792  cgr3com  36798  brofs2  36822  bj-idreseq  38063  areacirclem4  38609  paddasslem14  40870  lhpexle1  41045  cdlemk19w  42009  ismrc  43691  iocinico  44198  gneispb  45116  fourierdlem113  47198  sigaras  47834  sigarms  47835  plusmod5ne  48390  gpgusgralem  49123  lincresunit3lem3  49555  lincresunit3  49562