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 1087

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 1089

This theorem is referenced by:  3adantl2  1167  3adantr2  1170  fpropnf1  7307  cfcof  10346  axcclem  10529  enqeq  11006  leltletr  11384  ltleletr  11386  ixxssixx  13432  prodmolem2  16000  prodmo  16001  zprod  16002  muldvds1  16347  dvds2add  16356  dvds2sub  16357  dvdstr  16360  initoeu2lem2  18102  pospropd  18417  mndissubm  18862  csrgbinom  20279  smadiadetglem2  22719  ismbf3d  25728  mbfi1flimlem  25797  colinearalg  28963  frusgrnn0  29627  2wlkond  29990  2pthond  29995  2pthon3v  29996  umgr2adedgwlkonALT  30000  vdgn1frgrv2  30348  frgr2wwlkeqm  30383  bnj967  34941  bnj1110  34978  subgrwlk  35120  cgr3permute3  36031  cgr3com  36037  brofs2  36061  bj-idreseq  37148  areacirclem4  37691  paddasslem14  39810  lhpexle1  39985  cdlemk19w  40949  ismrc  42676  iocinico  43192  gneispb  44112  fourierdlem113  46158  sigaras  46794  sigarms  46795  plusmod5ne  47268  gpgusgralem  47900  lincresunit3lem3  48274  lincresunit3  48281