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  4821  fpropnf1  7242  fovcld  7516  find  7871  tz7.49c  8414  dif1en  9124  eqsup  9407  fimin2g  9450  mulcanenq  10913  elnpi  10941  divcan2  11845  divrec  11853  divcan3  11863  eliooord  13366  fzrev3  13551  modaddabs  13873  modaddmod  13874  muladdmodid  13875  modmulmod  13901  sqdiv  14086  swrdlend  14618  swrdnd  14619  ccats1pfxeqbi  14707  sqrmo  15217  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  dvdstr  16264  funcestrcsetclem9  18109  funcsetcestrclem9  18124  gsumccat  18768  domneq0  20617  znleval2  21465  redvr  21526  aspid  21784  scmatscmiddistr  22395  1marepvmarrepid  22462  mat2pmatghm  22617  pmatcollpw1lem1  22661  monmatcollpw  22666  pmatcollpwscmatlem2  22677  conncompss  23320  islly2  23371  elmptrab2  23715  tngngp3  24544  lmmcvg  25161  cmslsschl  25277  ivthicc  25359  aaliou3lem7  26257  logimcl  26478  qrngdiv  27535  etasslt  27725  ax5seg  28865  uhgr2edg  29135  umgr2edgneu  29141  uspgr1ewop  29175  iswlkg  29541  wlkonwlk  29590  trlontrl  29639  upgrwlkdvspth  29669  pthonpth  29678  spthonpthon  29681  uhgrwkspth  29685  usgr2wlkspthlem1  29687  usgr2wlkspthlem2  29688  usgr2wlkspth  29689  2pthon3v  29873  umgr2wlk  29879  rusgrnumwwlkg  29906  clwwisshclwws  29944  clwwlknp  29966  clwwlkfo  29979  clwwlknwwlkncl  29982  1pthond  30073  uhgr3cyclex  30111  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  numclwwlk3  30314  ajfuni  30788  funadj  31815  trleile  32897  isinftm  33135  bnj1098  34773  bnj546  34886  bnj998  34947  bnj1006  34950  bnj1173  34992  bnj1189  34999  cusgr3cyclex  35123  elnanelprv  35416  cgr3permute1  36036  cgr3com  36041  brifs2  36066  idinside  36072  btwnconn1  36089  lineunray  36135  wl-nfeqfb  37524  dmqsblocks  38845  riotasv2s  38951  lsatlspsn2  38985  3dim2  39462  paddasslem14  39827  4atexlemex6  40068  cdlemg10bALTN  40630  cdlemg44  40727  tendoplcl  40775  hdmap14lem14  41875  nnawordexg  43316  pm13.194  44401  fmulcl  45579  fmuldfeqlem1  45580  stoweidlem17  46015  stoweidlem31  46029  dfsalgen2  46339  sigaraf  46851  sigarmf  46852  elfzelfzlble  47322  dfclnbgr6  47856  dfnbgr6  47857  dfsclnbgr6  47858  isubgr3stgrlem4  47968  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  zlmodzxzscm  48345  divsub1dir  48506  elbigoimp  48545  digexp  48596  2arymptfv  48639  funcf2lem2  49071