Theorem 3simpc 1149

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 1129	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  1165  3adantr1  1168  pr1eqbg  4861  fpropnf1  7286  fovcld  7559  find  7917  tz7.49c  8484  dif1en  9198  eqsup  9493  fimin2g  9534  mulcanenq  10997  elnpi  11025  divcan2  11927  divrec  11935  divcan3  11945  eliooord  13442  fzrev3  13626  modaddabs  13945  modaddmod  13946  muladdmodid  13947  modmulmod  13973  sqdiv  14157  swrdlend  14687  swrdnd  14688  ccats1pfxeqbi  14776  sqrmo  15286  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  dvdstr  16327  funcestrcsetclem9  18203  funcsetcestrclem9  18218  gsumccat  18866  domneq0  20724  znleval2  21591  redvr  21652  aspid  21912  scmatscmiddistr  22529  1marepvmarrepid  22596  mat2pmatghm  22751  pmatcollpw1lem1  22795  monmatcollpw  22800  pmatcollpwscmatlem2  22811  conncompss  23456  islly2  23507  elmptrab2  23851  tngngp3  24692  lmmcvg  25308  cmslsschl  25424  ivthicc  25506  aaliou3lem7  26405  logimcl  26625  qrngdiv  27682  etasslt  27872  ax5seg  28967  uhgr2edg  29239  umgr2edgneu  29245  uspgr1ewop  29279  iswlkg  29645  wlkonwlk  29694  trlontrl  29743  upgrwlkdvspth  29771  pthonpth  29780  spthonpthon  29783  uhgrwkspth  29787  usgr2wlkspthlem1  29789  usgr2wlkspthlem2  29790  usgr2wlkspth  29791  2pthon3v  29972  umgr2wlk  29978  rusgrnumwwlkg  30005  clwwisshclwws  30043  clwwlknp  30065  clwwlkfo  30078  clwwlknwwlkncl  30081  1pthond  30172  uhgr3cyclex  30210  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  numclwwlk3  30413  ajfuni  30887  funadj  31914  trleile  32945  isinftm  33170  bnj1098  34775  bnj546  34888  bnj998  34949  bnj1006  34952  bnj1173  34994  bnj1189  35001  cusgr3cyclex  35120  elnanelprv  35413  cgr3permute1  36029  cgr3com  36034  brifs2  36059  idinside  36065  btwnconn1  36082  lineunray  36128  wl-nfeqfb  37516  riotasv2s  38939  lsatlspsn2  38973  3dim2  39450  paddasslem14  39815  4atexlemex6  40056  cdlemg10bALTN  40618  cdlemg44  40715  tendoplcl  40763  hdmap14lem14  41863  nnawordexg  43316  pm13.194  44407  fmulcl  45536  fmuldfeqlem1  45537  stoweidlem17  45972  stoweidlem31  45986  dfsalgen2  46296  sigaraf  46808  sigarmf  46809  elfzelfzlble  47270  dfclnbgr6  47779  dfnbgr6  47780  dfsclnbgr6  47781  isubgr3stgrlem4  47871  funcringcsetcALTV2lem9  48141  funcringcsetclem9ALTV  48164  zlmodzxzscm  48201  divsub1dir  48362  elbigoimp  48405  digexp  48456  2arymptfv  48499