Theorem 3simpc 1148

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  3adantl1  1164  3adantr1  1167  pr1eqbg  4856  fpropnf1  7268  fovcld  7538  find  7889  findOLD  7890  tz7.49c  8448  dif1en  9162  eqsup  9453  fimin2g  9494  mulcanenq  10957  elnpi  10985  divcan2  11884  diveq0  11886  divrec  11892  divcan3  11902  eliooord  13387  fzrev3  13571  modaddabs  13878  modaddmod  13879  muladdmodid  13880  modmulmod  13905  sqdiv  14090  swrdlend  14607  swrdnd  14608  ccats1pfxeqbi  14696  sqrmo  15202  muldvds2  16229  dvdscmul  16230  dvdsmulc  16231  dvdstr  16241  funcestrcsetclem9  18104  funcsetcestrclem9  18119  gsumccat  18758  domneq0  21113  znleval2  21330  redvr  21389  aspid  21648  scmatscmiddistr  22230  1marepvmarrepid  22297  mat2pmatghm  22452  pmatcollpw1lem1  22496  monmatcollpw  22501  pmatcollpwscmatlem2  22512  conncompss  23157  islly2  23208  elmptrab2  23552  tngngp3  24393  lmmcvg  25009  cmslsschl  25125  ivthicc  25207  aaliou3lem7  26098  logimcl  26314  qrngdiv  27363  etasslt  27551  ax5seg  28463  uhgr2edg  28732  umgr2edgneu  28738  uspgr1ewop  28772  iswlkg  29137  wlkonwlk  29186  trlontrl  29235  upgrwlkdvspth  29263  pthonpth  29272  spthonpthon  29275  uhgrwkspth  29279  usgr2wlkspthlem1  29281  usgr2wlkspthlem2  29282  usgr2wlkspth  29283  2pthon3v  29464  umgr2wlk  29470  rusgrnumwwlkg  29497  clwwisshclwws  29535  clwwlknp  29557  clwwlkfo  29570  clwwlknwwlkncl  29573  1pthond  29664  uhgr3cyclex  29702  numclwlk2lem2f  29897  numclwlk2lem2f1o  29899  numclwwlk3  29905  ajfuni  30379  funadj  31406  trleile  32408  isinftm  32597  bnj1098  34092  bnj546  34205  bnj998  34266  bnj1006  34269  bnj1173  34311  bnj1189  34318  cusgr3cyclex  34425  elnanelprv  34718  cgr3permute1  35324  cgr3com  35329  brifs2  35354  idinside  35360  btwnconn1  35377  lineunray  35423  gg-cncrng  35486  wl-nfeqfb  36708  riotasv2s  38131  lsatlspsn2  38165  3dim2  38642  paddasslem14  39007  4atexlemex6  39248  cdlemg10bALTN  39810  cdlemg44  39907  tendoplcl  39955  hdmap14lem14  41055  nnawordexg  42379  pm13.194  43473  fmulcl  44595  fmuldfeqlem1  44596  stoweidlem17  45031  stoweidlem31  45045  dfsalgen2  45355  sigaraf  45867  sigarmf  45868  elfzelfzlble  46327  funcringcsetcALTV2lem9  47030  funcringcsetclem9ALTV  47053  zlmodzxzscm  47121  divsub1dir  47285  elbigoimp  47329  digexp  47380  2arymptfv  47423