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  4824  fpropnf1  7245  fovcld  7519  find  7874  tz7.49c  8417  dif1en  9130  eqsup  9414  fimin2g  9457  mulcanenq  10920  elnpi  10948  divcan2  11852  divrec  11860  divcan3  11870  eliooord  13373  fzrev3  13558  modaddabs  13880  modaddmod  13881  muladdmodid  13882  modmulmod  13908  sqdiv  14093  swrdlend  14625  swrdnd  14626  ccats1pfxeqbi  14714  sqrmo  15224  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  dvdstr  16271  funcestrcsetclem9  18116  funcsetcestrclem9  18131  gsumccat  18775  domneq0  20624  znleval2  21472  redvr  21533  aspid  21791  scmatscmiddistr  22402  1marepvmarrepid  22469  mat2pmatghm  22624  pmatcollpw1lem1  22668  monmatcollpw  22673  pmatcollpwscmatlem2  22684  conncompss  23327  islly2  23378  elmptrab2  23722  tngngp3  24551  lmmcvg  25168  cmslsschl  25284  ivthicc  25366  aaliou3lem7  26264  logimcl  26485  qrngdiv  27542  etasslt  27732  ax5seg  28872  uhgr2edg  29142  umgr2edgneu  29148  uspgr1ewop  29182  iswlkg  29548  wlkonwlk  29597  trlontrl  29646  upgrwlkdvspth  29676  pthonpth  29685  spthonpthon  29688  uhgrwkspth  29692  usgr2wlkspthlem1  29694  usgr2wlkspthlem2  29695  usgr2wlkspth  29696  2pthon3v  29880  umgr2wlk  29886  rusgrnumwwlkg  29913  clwwisshclwws  29951  clwwlknp  29973  clwwlkfo  29986  clwwlknwwlkncl  29989  1pthond  30080  uhgr3cyclex  30118  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  numclwwlk3  30321  ajfuni  30795  funadj  31822  trleile  32904  isinftm  33142  bnj1098  34780  bnj546  34893  bnj998  34954  bnj1006  34957  bnj1173  34999  bnj1189  35006  cusgr3cyclex  35130  elnanelprv  35423  cgr3permute1  36043  cgr3com  36048  brifs2  36073  idinside  36079  btwnconn1  36096  lineunray  36142  wl-nfeqfb  37531  dmqsblocks  38852  riotasv2s  38958  lsatlspsn2  38992  3dim2  39469  paddasslem14  39834  4atexlemex6  40075  cdlemg10bALTN  40637  cdlemg44  40734  tendoplcl  40782  hdmap14lem14  41882  nnawordexg  43323  pm13.194  44408  fmulcl  45586  fmuldfeqlem1  45587  stoweidlem17  46022  stoweidlem31  46036  dfsalgen2  46346  sigaraf  46858  sigarmf  46859  elfzelfzlble  47326  dfclnbgr6  47860  dfnbgr6  47861  dfsclnbgr6  47862  isubgr3stgrlem4  47972  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  zlmodzxzscm  48349  divsub1dir  48510  elbigoimp  48549  digexp  48600  2arymptfv  48643  funcf2lem2  49075