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  1168  3adantr1  1171  pr1eqbg  4815  fpropnf1  7223  fovcld  7495  find  7847  tz7.49c  8387  dif1en  9098  eqsup  9371  fimin2g  9414  mulcanenq  10883  elnpi  10911  divcan2  11816  divrec  11824  divcan3  11834  eliooord  13333  fzrev3  13518  modaddabs  13843  modaddmod  13844  muladdmodid  13845  modmulmod  13871  sqdiv  14056  swrdlend  14589  swrdnd  14590  ccats1pfxeqbi  14677  sqrmo  15186  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  dvdstr  16233  funcestrcsetclem9  18083  funcsetcestrclem9  18098  gsumccat  18778  domneq0  20653  znleval2  21522  redvr  21584  aspid  21842  scmatscmiddistr  22464  1marepvmarrepid  22531  mat2pmatghm  22686  pmatcollpw1lem1  22730  monmatcollpw  22735  pmatcollpwscmatlem2  22746  conncompss  23389  islly2  23440  elmptrab2  23784  tngngp3  24612  lmmcvg  25229  cmslsschl  25345  ivthicc  25427  aaliou3lem7  26325  logimcl  26546  qrngdiv  27603  etaslts  27801  ax5seg  29023  uhgr2edg  29293  umgr2edgneu  29299  uspgr1ewop  29333  iswlkg  29699  wlkonwlk  29746  trlontrl  29794  upgrwlkdvspth  29824  pthonpth  29833  spthonpthon  29836  uhgrwkspth  29840  usgr2wlkspthlem1  29842  usgr2wlkspthlem2  29843  usgr2wlkspth  29844  2pthon3v  30028  umgr2wlk  30034  rusgrnumwwlkg  30064  clwwisshclwws  30102  clwwlknp  30124  clwwlkfo  30137  clwwlknwwlkncl  30140  1pthond  30231  uhgr3cyclex  30269  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  numclwwlk3  30472  ajfuni  30946  funadj  31973  trleile  33063  isinftm  33274  bnj1098  34959  bnj546  35071  bnj998  35132  bnj1006  35135  bnj1173  35177  bnj1189  35184  cusgr3cyclex  35349  elnanelprv  35642  cgr3permute1  36261  cgr3com  36266  brifs2  36291  idinside  36297  btwnconn1  36314  lineunray  36360  wl-nfeqfb  37785  dmqsblocks  39212  riotasv2s  39328  lsatlspsn2  39362  3dim2  39838  paddasslem14  40203  4atexlemex6  40444  cdlemg10bALTN  41006  cdlemg44  41103  tendoplcl  41151  hdmap14lem14  42251  nnawordexg  43678  pm13.194  44762  fmulcl  45935  fmuldfeqlem1  45936  stoweidlem17  46369  stoweidlem31  46383  dfsalgen2  46693  sigaraf  47205  sigarmf  47206  elfzelfzlble  47675  dfclnbgr6  48210  dfnbgr6  48211  dfsclnbgr6  48212  isubgr3stgrlem4  48323  funcringcsetcALTV2lem9  48652  funcringcsetclem9ALTV  48675  zlmodzxzscm  48711  divsub1dir  48871  elbigoimp  48910  digexp  48961  2arymptfv  49004  funcf2lem2  49435