Theorem 3simpc 1151

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Assertion

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

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	3adant1 1131	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3adantl1  1167  3adantr1  1170  pr1eqbg  4858  fpropnf1  7266  fovcld  7536  find  7887  findOLD  7888  tz7.49c  8446  dif1en  9160  eqsup  9451  fimin2g  9492  mulcanenq  10955  elnpi  10983  divcan2  11880  diveq0  11882  divrec  11888  divcan3  11898  eliooord  13383  fzrev3  13567  modaddabs  13874  modaddmod  13875  muladdmodid  13876  modmulmod  13901  sqdiv  14086  swrdlend  14603  swrdnd  14604  ccats1pfxeqbi  14692  sqrmo  15198  muldvds2  16225  dvdscmul  16226  dvdsmulc  16227  dvdstr  16237  funcestrcsetclem9  18100  funcsetcestrclem9  18115  gsumccat  18722  domneq0  20913  znleval2  21111  redvr  21170  aspid  21429  scmatscmiddistr  22010  1marepvmarrepid  22077  mat2pmatghm  22232  pmatcollpw1lem1  22276  monmatcollpw  22281  pmatcollpwscmatlem2  22292  conncompss  22937  islly2  22988  elmptrab2  23332  tngngp3  24173  lmmcvg  24778  cmslsschl  24894  ivthicc  24975  aaliou3lem7  25862  logimcl  26078  qrngdiv  27127  etasslt  27314  ax5seg  28196  uhgr2edg  28465  umgr2edgneu  28471  uspgr1ewop  28505  iswlkg  28870  wlkonwlk  28919  trlontrl  28968  upgrwlkdvspth  28996  pthonpth  29005  spthonpthon  29008  uhgrwkspth  29012  usgr2wlkspthlem1  29014  usgr2wlkspthlem2  29015  usgr2wlkspth  29016  2pthon3v  29197  umgr2wlk  29203  rusgrnumwwlkg  29230  clwwisshclwws  29268  clwwlknp  29290  clwwlkfo  29303  clwwlknwwlkncl  29306  1pthond  29397  uhgr3cyclex  29435  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  numclwwlk3  29638  ajfuni  30112  funadj  31139  trleile  32141  isinftm  32327  bnj1098  33794  bnj546  33907  bnj998  33968  bnj1006  33971  bnj1173  34013  bnj1189  34020  cusgr3cyclex  34127  elnanelprv  34420  cgr3permute1  35020  cgr3com  35025  brifs2  35050  idinside  35056  btwnconn1  35073  lineunray  35119  wl-nfeqfb  36405  riotasv2s  37828  lsatlspsn2  37862  3dim2  38339  paddasslem14  38704  4atexlemex6  38945  cdlemg10bALTN  39507  cdlemg44  39604  tendoplcl  39652  hdmap14lem14  40752  nnawordexg  42077  pm13.194  43171  fmulcl  44297  fmuldfeqlem1  44298  stoweidlem17  44733  stoweidlem31  44747  dfsalgen2  45057  sigaraf  45569  sigarmf  45570  elfzelfzlble  46029  funcringcsetcALTV2lem9  46942  funcringcsetclem9ALTV  46965  zlmodzxzscm  47033  divsub1dir  47198  elbigoimp  47242  digexp  47293  2arymptfv  47336