Theorem 3simpb 1052

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3simpb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Proof of Theorem 3simpb

Step	Hyp	Ref	Expression
1		3ancomb 1040	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
2		3simpa 1051	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝜑 ∧ 𝜒))
3	1, 2	sylbi 206	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3adant2  1073  3adantl2  1211  3adantr2  1214  cfcof  8979  axcclem  9162  enqeq  9635  ltleletr  10009  ixxssixx  12060  prodmolem2  14504  prodmo  14505  zprod  14506  muldvds1  14844  dvds2add  14853  dvds2sub  14854  dvdstr  14856  initoeu2lem2  16488  pospropd  16957  csrgbinom  18369  smadiadetglem2  20297  ismbf3d  23227  mbfi1flimlem  23295  colinearalg  25590  2pthon  26132  constr3trllem2  26179  wlkiswwlkinj  26246  2wlkonotv  26404  usg2spthonot  26415  usg2spthonot0  26416  vdn1frgrav2  26552  vdgn1frgrav2  26553  bnj967  30269  bnj1110  30304  cgr3permute3  31324  cgr3com  31330  brofs2  31354  areacirclem4  32673  paddasslem14  34137  lhpexle1  34312  cdlemk19w  35278  ismrc  36282  iocinico  36816  gneispb  37449  fourierdlem113  39112  sigaras  39693  sigarms  39694  leltletr  39940  fpropnf1  40337  frusgrnn0  40771  wlkwwlkinj  41093  21wlkond  41144  2pthond  41149  2pthon3v-av  41150  umgr2adedgwlkonALT  41154  usgr2wspthons3  41167  vdgn1frgrv2  41466  av-extwwlkfab  41520  lincresunit3lem3  42057  lincresunit3  42064