Theorem 3simpc 1168

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl1  1185  3adantr1  1188  pr1eqbg  4815  fpropnf1  7294  fovcld  7570  find  7931  tz7.49c  8484  dif1en  9205  eqsup  9475  fimin2g  9518  mulcanenq  11072  elnpi  11100  divcan2  12009  divrec  12017  divcan3  12027  eliooord  13563  fzrev3  13751  modaddabs  14078  modaddmod  14079  muladdmodid  14080  modmulmod  14106  sqdiv  14291  swrdlend  14831  swrdnd  14832  ccats1pfxeqbi  14919  sqrmo  15447  muldvds2  16480  dvdscmul  16481  dvdsmulc  16482  dvdstr  16493  funcestrcsetclem9  18351  funcsetcestrclem9  18366  gsumccat  19066  rng1zr  20434  srg1zr  20471  domneq0  20990  znleval2  21891  redvr  21953  aspid  22212  scmatscmiddistr  22853  1marepvmarrepid  22920  mat2pmatghm  23078  pmatcollpw1lem1  23122  monmatcollpw  23127  pmatcollpwscmatlem2  23138  conncompss  23781  islly2  23833  elmptrab2  24177  tngngp3  25005  lmmcvg  25612  cmslsschl  25728  ivthicc  25809  aaliou3lem7  26706  logimcl  26927  qrngdiv  27981  etaslts  28209  ax5seg  29546  uhgr2edg  29819  umgr2edgneu  29825  uspgr1ewop  29859  iswlkg  30224  wlkonwlk  30271  trlontrl  30323  upgrwlkdvspth  30355  pthonpth  30364  spthonpthon  30367  uhgrwkspth  30371  usgr2wlkspthlem1  30373  usgr2wlkspthlem2  30374  usgr2wlkspth  30375  2pthon3v  30562  umgr2wlk  30568  rusgrnumwwlkg  30598  clwwisshclwws  30636  clwwlknp  30658  clwwlkfo  30671  clwwlknwwlkncl  30674  1pthond  30765  uhgr3cyclex  30813  numclwlk2lem2f  31008  numclwlk2lem2f1o  31010  numclwwlk3  31016  ajfuni  31491  funadj  32518  trleile  33602  isinftm  33812  bnj1098  35484  bnj546  35596  bnj998  35657  bnj1006  35660  bnj1173  35702  bnj1189  35709  onvfowev  36050  cusgr3cyclex  36068  elnanelprv  36361  cgr3permute1  36991  cgr3com  36996  brifs2  37021  idinside  37027  btwnconn1  37044  lineunray  37090  wl-nfeqfb  38660  dmqsblocks  40091  riotasv2s  40207  lsatlspsn2  40241  3dim2  40717  paddasslem14  41082  4atexlemex6  41323  cdlemg10bALTN  41885  cdlemg44  41982  tendoplcl  42030  hdmap14lem14  43130  nnawordexg  44521  pm13.194  45588  fmulcl  46798  fmuldfeqlem1  46799  stoweidlem17  47232  stoweidlem31  47246  dfsalgen2  47556  sigaraf  48068  sigarmf  48069  elfzelfzlble  48596  nprmmul2  48815  dfclnbgr6  49159  dfnbgr6  49160  dfsclnbgr6  49161  isubgr3stgrlem4  49272  funcringcsetcALTV2lem9  49600  funcringcsetclem9ALTV  49623  zlmodzxzscm  49674  divsub1dir  49834  elbigoimp  49873  digexp  49924  2arymptfv  49967  elixpmpt  50209  funcf2lem2  50401