Theorem 3simpc 1151

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

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

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 1089

This theorem is referenced by:  3adantl1  1167  3adantr1  1170  pr1eqbg  4857  fpropnf1  7287  fovcld  7560  find  7917  tz7.49c  8486  dif1en  9200  eqsup  9496  fimin2g  9537  mulcanenq  11000  elnpi  11028  divcan2  11930  divrec  11938  divcan3  11948  eliooord  13446  fzrev3  13630  modaddabs  13949  modaddmod  13950  muladdmodid  13951  modmulmod  13977  sqdiv  14161  swrdlend  14691  swrdnd  14692  ccats1pfxeqbi  14780  sqrmo  15290  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  dvdstr  16331  funcestrcsetclem9  18193  funcsetcestrclem9  18208  gsumccat  18854  domneq0  20708  znleval2  21574  redvr  21635  aspid  21895  scmatscmiddistr  22514  1marepvmarrepid  22581  mat2pmatghm  22736  pmatcollpw1lem1  22780  monmatcollpw  22785  pmatcollpwscmatlem2  22796  conncompss  23441  islly2  23492  elmptrab2  23836  tngngp3  24677  lmmcvg  25295  cmslsschl  25411  ivthicc  25493  aaliou3lem7  26391  logimcl  26611  qrngdiv  27668  etasslt  27858  ax5seg  28953  uhgr2edg  29225  umgr2edgneu  29231  uspgr1ewop  29265  iswlkg  29631  wlkonwlk  29680  trlontrl  29729  upgrwlkdvspth  29759  pthonpth  29768  spthonpthon  29771  uhgrwkspth  29775  usgr2wlkspthlem1  29777  usgr2wlkspthlem2  29778  usgr2wlkspth  29779  2pthon3v  29963  umgr2wlk  29969  rusgrnumwwlkg  29996  clwwisshclwws  30034  clwwlknp  30056  clwwlkfo  30069  clwwlknwwlkncl  30072  1pthond  30163  uhgr3cyclex  30201  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  numclwwlk3  30404  ajfuni  30878  funadj  31905  trleile  32961  isinftm  33188  bnj1098  34797  bnj546  34910  bnj998  34971  bnj1006  34974  bnj1173  35016  bnj1189  35023  cusgr3cyclex  35141  elnanelprv  35434  cgr3permute1  36049  cgr3com  36054  brifs2  36079  idinside  36085  btwnconn1  36102  lineunray  36148  wl-nfeqfb  37537  riotasv2s  38959  lsatlspsn2  38993  3dim2  39470  paddasslem14  39835  4atexlemex6  40076  cdlemg10bALTN  40638  cdlemg44  40735  tendoplcl  40783  hdmap14lem14  41883  nnawordexg  43340  pm13.194  44431  fmulcl  45596  fmuldfeqlem1  45597  stoweidlem17  46032  stoweidlem31  46046  dfsalgen2  46356  sigaraf  46868  sigarmf  46869  elfzelfzlble  47333  dfclnbgr6  47842  dfnbgr6  47843  dfsclnbgr6  47844  isubgr3stgrlem4  47936  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  zlmodzxzscm  48273  divsub1dir  48434  elbigoimp  48477  digexp  48528  2arymptfv  48571  funcf2lem2  48915