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  4813  fpropnf1  7213  fovcld  7485  find  7837  tz7.49c  8377  dif1en  9086  eqsup  9359  fimin2g  9402  mulcanenq  10871  elnpi  10899  divcan2  11804  divrec  11812  divcan3  11822  eliooord  13321  fzrev3  13506  modaddabs  13831  modaddmod  13832  muladdmodid  13833  modmulmod  13859  sqdiv  14044  swrdlend  14577  swrdnd  14578  ccats1pfxeqbi  14665  sqrmo  15174  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  dvdstr  16221  funcestrcsetclem9  18071  funcsetcestrclem9  18086  gsumccat  18766  domneq0  20641  znleval2  21510  redvr  21572  aspid  21830  scmatscmiddistr  22452  1marepvmarrepid  22519  mat2pmatghm  22674  pmatcollpw1lem1  22718  monmatcollpw  22723  pmatcollpwscmatlem2  22734  conncompss  23377  islly2  23428  elmptrab2  23772  tngngp3  24600  lmmcvg  25217  cmslsschl  25333  ivthicc  25415  aaliou3lem7  26313  logimcl  26534  qrngdiv  27591  etaslts  27789  ax5seg  29011  uhgr2edg  29281  umgr2edgneu  29287  uspgr1ewop  29321  iswlkg  29687  wlkonwlk  29734  trlontrl  29782  upgrwlkdvspth  29812  pthonpth  29821  spthonpthon  29824  uhgrwkspth  29828  usgr2wlkspthlem1  29830  usgr2wlkspthlem2  29831  usgr2wlkspth  29832  2pthon3v  30016  umgr2wlk  30022  rusgrnumwwlkg  30052  clwwisshclwws  30090  clwwlknp  30112  clwwlkfo  30125  clwwlknwwlkncl  30128  1pthond  30219  uhgr3cyclex  30257  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  numclwwlk3  30460  ajfuni  30934  funadj  31961  trleile  33053  isinftm  33263  bnj1098  34939  bnj546  35052  bnj998  35113  bnj1006  35116  bnj1173  35158  bnj1189  35165  cusgr3cyclex  35330  elnanelprv  35623  cgr3permute1  36242  cgr3com  36247  brifs2  36272  idinside  36278  btwnconn1  36295  lineunray  36341  wl-nfeqfb  37737  dmqsblocks  39108  riotasv2s  39214  lsatlspsn2  39248  3dim2  39724  paddasslem14  40089  4atexlemex6  40330  cdlemg10bALTN  40892  cdlemg44  40989  tendoplcl  41037  hdmap14lem14  42137  nnawordexg  43565  pm13.194  44649  fmulcl  45823  fmuldfeqlem1  45824  stoweidlem17  46257  stoweidlem31  46271  dfsalgen2  46581  sigaraf  47093  sigarmf  47094  elfzelfzlble  47563  dfclnbgr6  48098  dfnbgr6  48099  dfsclnbgr6  48100  isubgr3stgrlem4  48211  funcringcsetcALTV2lem9  48540  funcringcsetclem9ALTV  48563  zlmodzxzscm  48599  divsub1dir  48759  elbigoimp  48798  digexp  48849  2arymptfv  48892  funcf2lem2  49323