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  4808  fpropnf1  7207  fovcld  7479  find  7831  tz7.49c  8371  dif1en  9077  eqsup  9346  fimin2g  9389  mulcanenq  10857  elnpi  10885  divcan2  11790  divrec  11798  divcan3  11808  eliooord  13311  fzrev3  13496  modaddabs  13821  modaddmod  13822  muladdmodid  13823  modmulmod  13849  sqdiv  14034  swrdlend  14567  swrdnd  14568  ccats1pfxeqbi  14655  sqrmo  15164  muldvds2  16198  dvdscmul  16199  dvdsmulc  16200  dvdstr  16211  funcestrcsetclem9  18060  funcsetcestrclem9  18075  gsumccat  18755  domneq0  20629  znleval2  21498  redvr  21560  aspid  21818  scmatscmiddistr  22429  1marepvmarrepid  22496  mat2pmatghm  22651  pmatcollpw1lem1  22695  monmatcollpw  22700  pmatcollpwscmatlem2  22711  conncompss  23354  islly2  23405  elmptrab2  23749  tngngp3  24577  lmmcvg  25194  cmslsschl  25310  ivthicc  25392  aaliou3lem7  26290  logimcl  26511  qrngdiv  27568  etasslt  27760  ax5seg  28923  uhgr2edg  29193  umgr2edgneu  29199  uspgr1ewop  29233  iswlkg  29599  wlkonwlk  29646  trlontrl  29694  upgrwlkdvspth  29724  pthonpth  29733  spthonpthon  29736  uhgrwkspth  29740  usgr2wlkspthlem1  29742  usgr2wlkspthlem2  29743  usgr2wlkspth  29744  2pthon3v  29928  umgr2wlk  29934  rusgrnumwwlkg  29964  clwwisshclwws  30002  clwwlknp  30024  clwwlkfo  30037  clwwlknwwlkncl  30040  1pthond  30131  uhgr3cyclex  30169  numclwlk2lem2f  30364  numclwlk2lem2f1o  30366  numclwwlk3  30372  ajfuni  30846  funadj  31873  trleile  32959  isinftm  33157  bnj1098  34802  bnj546  34915  bnj998  34976  bnj1006  34979  bnj1173  35021  bnj1189  35028  cusgr3cyclex  35187  elnanelprv  35480  cgr3permute1  36099  cgr3com  36104  brifs2  36129  idinside  36135  btwnconn1  36152  lineunray  36198  wl-nfeqfb  37587  dmqsblocks  38957  riotasv2s  39063  lsatlspsn2  39097  3dim2  39573  paddasslem14  39938  4atexlemex6  40179  cdlemg10bALTN  40741  cdlemg44  40838  tendoplcl  40886  hdmap14lem14  41986  nnawordexg  43425  pm13.194  44510  fmulcl  45686  fmuldfeqlem1  45687  stoweidlem17  46120  stoweidlem31  46134  dfsalgen2  46444  sigaraf  46956  sigarmf  46957  elfzelfzlble  47426  dfclnbgr6  47961  dfnbgr6  47962  dfsclnbgr6  47963  isubgr3stgrlem4  48074  funcringcsetcALTV2lem9  48403  funcringcsetclem9ALTV  48426  zlmodzxzscm  48462  divsub1dir  48623  elbigoimp  48662  digexp  48713  2arymptfv  48756  funcf2lem2  49188