Theorem 3simpc 1150

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adantl1  1167  3adantr1  1170  pr1eqbg  4809  fpropnf1  7201  fovcld  7473  find  7825  tz7.49c  8365  dif1en  9071  eqsup  9340  fimin2g  9383  mulcanenq  10848  elnpi  10876  divcan2  11781  divrec  11789  divcan3  11799  eliooord  13302  fzrev3  13487  modaddabs  13812  modaddmod  13813  muladdmodid  13814  modmulmod  13840  sqdiv  14025  swrdlend  14558  swrdnd  14559  ccats1pfxeqbi  14646  sqrmo  15155  muldvds2  16189  dvdscmul  16190  dvdsmulc  16191  dvdstr  16202  funcestrcsetclem9  18051  funcsetcestrclem9  18066  gsumccat  18746  domneq0  20621  znleval2  21490  redvr  21552  aspid  21810  scmatscmiddistr  22421  1marepvmarrepid  22488  mat2pmatghm  22643  pmatcollpw1lem1  22687  monmatcollpw  22692  pmatcollpwscmatlem2  22703  conncompss  23346  islly2  23397  elmptrab2  23741  tngngp3  24569  lmmcvg  25186  cmslsschl  25302  ivthicc  25384  aaliou3lem7  26282  logimcl  26503  qrngdiv  27560  etasslt  27752  ax5seg  28914  uhgr2edg  29184  umgr2edgneu  29190  uspgr1ewop  29224  iswlkg  29590  wlkonwlk  29637  trlontrl  29685  upgrwlkdvspth  29715  pthonpth  29724  spthonpthon  29727  uhgrwkspth  29731  usgr2wlkspthlem1  29733  usgr2wlkspthlem2  29734  usgr2wlkspth  29735  2pthon3v  29919  umgr2wlk  29925  rusgrnumwwlkg  29952  clwwisshclwws  29990  clwwlknp  30012  clwwlkfo  30025  clwwlknwwlkncl  30028  1pthond  30119  uhgr3cyclex  30157  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  numclwwlk3  30360  ajfuni  30834  funadj  31861  trleile  32947  isinftm  33145  bnj1098  34790  bnj546  34903  bnj998  34964  bnj1006  34967  bnj1173  35009  bnj1189  35016  cusgr3cyclex  35168  elnanelprv  35461  cgr3permute1  36081  cgr3com  36086  brifs2  36111  idinside  36117  btwnconn1  36134  lineunray  36180  wl-nfeqfb  37569  dmqsblocks  38890  riotasv2s  38996  lsatlspsn2  39030  3dim2  39506  paddasslem14  39871  4atexlemex6  40112  cdlemg10bALTN  40674  cdlemg44  40771  tendoplcl  40819  hdmap14lem14  41919  nnawordexg  43359  pm13.194  44444  fmulcl  45620  fmuldfeqlem1  45621  stoweidlem17  46054  stoweidlem31  46068  dfsalgen2  46378  sigaraf  46890  sigarmf  46891  elfzelfzlble  47351  dfclnbgr6  47886  dfnbgr6  47887  dfsclnbgr6  47888  isubgr3stgrlem4  47999  funcringcsetcALTV2lem9  48328  funcringcsetclem9ALTV  48351  zlmodzxzscm  48387  divsub1dir  48548  elbigoimp  48587  digexp  48638  2arymptfv  48681  funcf2lem2  49113