Theorem 3simpc 1146

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 1126	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adantl1  1162  3adantr1  1165  pr1eqbg  4789  fpropnf1  7027  find  7609  tz7.49c  8084  eqsup  8922  fimin2g  8963  mulcanenq  10384  elnpi  10412  divcan2  11308  diveq0  11310  divrec  11316  divcan3  11326  eliooord  12799  fzrev3  12976  modaddabs  13280  modaddmod  13281  muladdmodid  13282  modmulmod  13307  sqdiv  13490  swrdlend  14017  swrdnd  14018  ccats1pfxeqbi  14106  sqrmo  14613  muldvds2  15637  dvdscmul  15638  dvdsmulc  15639  dvdstr  15648  funcestrcsetclem9  17400  funcsetcestrclem9  17415  gsumccat  18008  domneq0  20072  aspid  20106  znleval2  20704  redvr  20763  scmatscmiddistr  21119  1marepvmarrepid  21186  mat2pmatghm  21340  pmatcollpw1lem1  21384  monmatcollpw  21389  pmatcollpwscmatlem2  21400  conncompss  22043  islly2  22094  elmptrab2  22438  tngngp3  23267  lmmcvg  23866  cmslsschl  23982  ivthicc  24061  aaliou3lem7  24940  logimcl  25155  qrngdiv  26202  ax5seg  26726  uhgr2edg  26992  umgr2edgneu  26998  uspgr1ewop  27032  iswlkg  27397  wlkonwlk  27446  trlontrl  27494  upgrwlkdvspth  27522  pthonpth  27531  spthonpthon  27534  uhgrwkspth  27538  usgr2wlkspthlem1  27540  usgr2wlkspthlem2  27541  usgr2wlkspth  27542  2pthon3v  27724  umgr2wlk  27730  rusgrnumwwlkg  27757  clwwisshclwws  27795  clwwlknp  27817  clwwlkfo  27831  clwwlknwwlkncl  27834  1pthond  27925  uhgr3cyclex  27963  numclwlk2lem2f  28158  numclwlk2lem2f1o  28160  numclwwlk3  28166  ajfuni  28638  funadj  29665  fovcld  30387  trleile  30655  isinftm  30812  bnj1098  32057  bnj546  32170  bnj998  32231  bnj1006  32234  bnj1173  32276  bnj1189  32283  cusgr3cyclex  32385  elnanelprv  32678  cgr3permute1  33511  cgr3com  33516  brifs2  33541  idinside  33547  btwnconn1  33564  lineunray  33610  wl-nfeqfb  34778  riotasv2s  36096  lsatlspsn2  36130  3dim2  36606  paddasslem14  36971  4atexlemex6  37212  cdlemg10bALTN  37774  cdlemg44  37871  tendoplcl  37919  hdmap14lem14  39019  pm13.194  40751  fmulcl  41869  fmuldfeqlem1  41870  stoweidlem17  42309  stoweidlem31  42323  dfsalgen2  42631  sigaraf  43117  sigarmf  43118  elfzelfzlble  43528  funcringcsetcALTV2lem9  44322  funcringcsetclem9ALTV  44345  zlmodzxzscm  44412  divsub1dir  44579  elbigoimp  44623  digexp  44674