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  7272  cfcof  10276  axcclem  10459  enqeq  10937  leltletr  11319  ltleletr  11321  ixxssixx  13404  prodmolem2  16015  prodmo  16016  zprod  16017  muldvds1  16363  dvds2add  16373  dvds2sub  16374  dvdstr  16377  initoeu2lem2  18097  pospropd  18406  mndissubm  18896  csrgbinom  20345  smadiadetglem2  22866  ismbf3d  25850  mbfi1flimlem  25918  colinearalg  29297  frusgrnn0  29958  2wlkond  30323  2pthond  30328  2pthon3v  30329  umgr2adedgwlkonALT  30333  vdgn1frgrv2  30684  frgr2wwlkeqm  30719  bnj967  35365  bnj1110  35402  fineqvinfep  35562  subgrwlk  35645  cgr3permute3  36560  cgr3com  36566  brofs2  36590  bj-idreseq  37847  areacirclem4  38403  paddasslem14  40648  lhpexle1  40823  cdlemk19w  41787  ismrc  43473  iocinico  43980  gneispb  44898  fourierdlem113  46974  sigaras  47610  sigarms  47611  plusmod5ne  48129  gpgusgralem  48862  lincresunit3lem3  49295  lincresunit3  49302