Theorem 3simpc 1149

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3adantl1  1165  3adantr1  1168  pr1eqbg  4787  fpropnf1  7140  find  7743  findOLD  7744  tz7.49c  8277  eqsup  9215  fimin2g  9256  mulcanenq  10716  elnpi  10744  divcan2  11641  diveq0  11643  divrec  11649  divcan3  11659  eliooord  13138  fzrev3  13322  modaddabs  13629  modaddmod  13630  muladdmodid  13631  modmulmod  13656  sqdiv  13841  swrdlend  14366  swrdnd  14367  ccats1pfxeqbi  14455  sqrmo  14963  muldvds2  15991  dvdscmul  15992  dvdsmulc  15993  dvdstr  16003  funcestrcsetclem9  17865  funcsetcestrclem9  17880  gsumccat  18480  domneq0  20568  znleval2  20763  redvr  20822  aspid  21079  scmatscmiddistr  21657  1marepvmarrepid  21724  mat2pmatghm  21879  pmatcollpw1lem1  21923  monmatcollpw  21928  pmatcollpwscmatlem2  21939  conncompss  22584  islly2  22635  elmptrab2  22979  tngngp3  23820  lmmcvg  24425  cmslsschl  24541  ivthicc  24622  aaliou3lem7  25509  logimcl  25725  qrngdiv  26772  ax5seg  27306  uhgr2edg  27575  umgr2edgneu  27581  uspgr1ewop  27615  iswlkg  27980  wlkonwlk  28030  trlontrl  28079  upgrwlkdvspth  28107  pthonpth  28116  spthonpthon  28119  uhgrwkspth  28123  usgr2wlkspthlem1  28125  usgr2wlkspthlem2  28126  usgr2wlkspth  28127  2pthon3v  28308  umgr2wlk  28314  rusgrnumwwlkg  28341  clwwisshclwws  28379  clwwlknp  28401  clwwlkfo  28414  clwwlknwwlkncl  28417  1pthond  28508  uhgr3cyclex  28546  numclwlk2lem2f  28741  numclwlk2lem2f1o  28743  numclwwlk3  28749  ajfuni  29221  funadj  30248  fovcld  30975  trleile  31249  isinftm  31435  bnj1098  32763  bnj546  32876  bnj998  32937  bnj1006  32940  bnj1173  32982  bnj1189  32989  cusgr3cyclex  33098  elnanelprv  33391  etasslt  34007  cgr3permute1  34350  cgr3com  34355  brifs2  34380  idinside  34386  btwnconn1  34403  lineunray  34449  wl-nfeqfb  35695  riotasv2s  36972  lsatlspsn2  37006  3dim2  37482  paddasslem14  37847  4atexlemex6  38088  cdlemg10bALTN  38650  cdlemg44  38747  tendoplcl  38795  hdmap14lem14  39895  pm13.194  42030  fmulcl  43122  fmuldfeqlem1  43123  stoweidlem17  43558  stoweidlem31  43572  dfsalgen2  43880  sigaraf  44369  sigarmf  44370  elfzelfzlble  44813  funcringcsetcALTV2lem9  45602  funcringcsetclem9ALTV  45625  zlmodzxzscm  45693  divsub1dir  45858  elbigoimp  45902  digexp  45953  2arymptfv  45996