Theorem 3simpc 1166

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 23	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	3adant1 1146	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adantl1  1183  3adantr1  1186  pr1eqbg  4818  fpropnf1  7255  fovcld  7527  find  7880  tz7.49c  8421  dif1en  9134  eqsup  9404  fimin2g  9447  mulcanenq  10933  elnpi  10961  divcan2  11868  divrec  11876  divcan3  11886  eliooord  13423  fzrev3  13609  modaddabs  13935  modaddmod  13936  muladdmodid  13937  modmulmod  13963  sqdiv  14148  swrdlend  14681  swrdnd  14682  ccats1pfxeqbi  14769  sqrmo  15292  muldvds2  16329  dvdscmul  16330  dvdsmulc  16331  dvdstr  16342  funcestrcsetclem9  18194  funcsetcestrclem9  18209  gsumccat  18890  rng1zr  20251  srg1zr  20288  domneq0  20784  znleval2  21665  redvr  21727  aspid  21984  scmatscmiddistr  22626  1marepvmarrepid  22693  mat2pmatghm  22848  pmatcollpw1lem1  22892  monmatcollpw  22897  pmatcollpwscmatlem2  22908  conncompss  23551  islly2  23602  elmptrab2  23946  tngngp3  24774  lmmcvg  25381  cmslsschl  25497  ivthicc  25578  aaliou3lem7  26471  logimcl  26692  qrngdiv  27746  etaslts  27944  ax5seg  29197  uhgr2edg  29467  umgr2edgneu  29473  uspgr1ewop  29507  iswlkg  29872  wlkonwlk  29919  trlontrl  29967  upgrwlkdvspth  29997  pthonpth  30006  spthonpthon  30009  uhgrwkspth  30013  usgr2wlkspthlem1  30015  usgr2wlkspthlem2  30016  usgr2wlkspth  30017  2pthon3v  30201  umgr2wlk  30207  rusgrnumwwlkg  30237  clwwisshclwws  30275  clwwlknp  30297  clwwlkfo  30310  clwwlknwwlkncl  30313  1pthond  30404  uhgr3cyclex  30442  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  numclwwlk3  30645  ajfuni  31120  funadj  32147  trleile  33204  isinftm  33414  bnj1098  35089  bnj546  35201  bnj998  35262  bnj1006  35265  bnj1173  35307  bnj1189  35314  onvfowev  35471  cusgr3cyclex  35499  elnanelprv  35792  cgr3permute1  36411  cgr3com  36416  brifs2  36441  idinside  36447  btwnconn1  36464  lineunray  36510  wl-nfeqfb  38051  dmqsblocks  39478  riotasv2s  39594  lsatlspsn2  39628  3dim2  40104  paddasslem14  40469  4atexlemex6  40710  cdlemg10bALTN  41272  cdlemg44  41369  tendoplcl  41417  hdmap14lem14  42517  nnawordexg  43916  pm13.194  44986  fmulcl  46155  fmuldfeqlem1  46156  stoweidlem17  46589  stoweidlem31  46603  dfsalgen2  46913  sigaraf  47425  sigarmf  47426  elfzelfzlble  47913  nprmmul2  48132  dfclnbgr6  48476  dfnbgr6  48477  dfsclnbgr6  48478  isubgr3stgrlem4  48589  funcringcsetcALTV2lem9  48918  funcringcsetclem9ALTV  48941  zlmodzxzscm  48988  divsub1dir  49148  elbigoimp  49187  digexp  49238  2arymptfv  49281  funcf2lem2  49711