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  4811  fpropnf1  7208  fovcld  7480  find  7835  tz7.49c  8375  dif1en  9084  eqsup  9365  fimin2g  9408  mulcanenq  10873  elnpi  10901  divcan2  11805  divrec  11813  divcan3  11823  eliooord  13326  fzrev3  13511  modaddabs  13833  modaddmod  13834  muladdmodid  13835  modmulmod  13861  sqdiv  14046  swrdlend  14578  swrdnd  14579  ccats1pfxeqbi  14666  sqrmo  15176  muldvds2  16210  dvdscmul  16211  dvdsmulc  16212  dvdstr  16223  funcestrcsetclem9  18072  funcsetcestrclem9  18087  gsumccat  18733  domneq0  20611  znleval2  21480  redvr  21542  aspid  21800  scmatscmiddistr  22411  1marepvmarrepid  22478  mat2pmatghm  22633  pmatcollpw1lem1  22677  monmatcollpw  22682  pmatcollpwscmatlem2  22693  conncompss  23336  islly2  23387  elmptrab2  23731  tngngp3  24560  lmmcvg  25177  cmslsschl  25293  ivthicc  25375  aaliou3lem7  26273  logimcl  26494  qrngdiv  27551  etasslt  27742  ax5seg  28901  uhgr2edg  29171  umgr2edgneu  29177  uspgr1ewop  29211  iswlkg  29577  wlkonwlk  29624  trlontrl  29672  upgrwlkdvspth  29702  pthonpth  29711  spthonpthon  29714  uhgrwkspth  29718  usgr2wlkspthlem1  29720  usgr2wlkspthlem2  29721  usgr2wlkspth  29722  2pthon3v  29906  umgr2wlk  29912  rusgrnumwwlkg  29939  clwwisshclwws  29977  clwwlknp  29999  clwwlkfo  30012  clwwlknwwlkncl  30015  1pthond  30106  uhgr3cyclex  30144  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  numclwwlk3  30347  ajfuni  30821  funadj  31848  trleile  32926  isinftm  33133  bnj1098  34749  bnj546  34862  bnj998  34923  bnj1006  34926  bnj1173  34968  bnj1189  34975  cusgr3cyclex  35108  elnanelprv  35401  cgr3permute1  36021  cgr3com  36026  brifs2  36051  idinside  36057  btwnconn1  36074  lineunray  36120  wl-nfeqfb  37509  dmqsblocks  38830  riotasv2s  38936  lsatlspsn2  38970  3dim2  39447  paddasslem14  39812  4atexlemex6  40053  cdlemg10bALTN  40615  cdlemg44  40712  tendoplcl  40760  hdmap14lem14  41860  nnawordexg  43300  pm13.194  44385  fmulcl  45563  fmuldfeqlem1  45564  stoweidlem17  45999  stoweidlem31  46013  dfsalgen2  46323  sigaraf  46835  sigarmf  46836  elfzelfzlble  47306  dfclnbgr6  47841  dfnbgr6  47842  dfsclnbgr6  47843  isubgr3stgrlem4  47954  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306  zlmodzxzscm  48342  divsub1dir  48503  elbigoimp  48542  digexp  48593  2arymptfv  48636  funcf2lem2  49068