Theorem 3simpc 1162

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adantl1  1179  3adantr1  1182  pr1eqbg  4814  fpropnf1  7247  fovcld  7519  find  7872  tz7.49c  8412  dif1en  9126  eqsup  9399  fimin2g  9442  mulcanenq  10915  elnpi  10943  divcan2  11850  divrec  11858  divcan3  11868  eliooord  13406  fzrev3  13592  modaddabs  13918  modaddmod  13919  muladdmodid  13920  modmulmod  13946  sqdiv  14131  swrdlend  14664  swrdnd  14665  ccats1pfxeqbi  14752  sqrmo  15261  muldvds2  16298  dvdscmul  16299  dvdsmulc  16300  dvdstr  16311  funcestrcsetclem9  18163  funcsetcestrclem9  18178  gsumccat  18858  domneq0  20737  znleval2  21587  redvr  21649  aspid  21906  scmatscmiddistr  22548  1marepvmarrepid  22615  mat2pmatghm  22770  pmatcollpw1lem1  22814  monmatcollpw  22819  pmatcollpwscmatlem2  22830  conncompss  23473  islly2  23524  elmptrab2  23868  tngngp3  24696  lmmcvg  25303  cmslsschl  25419  ivthicc  25500  aaliou3lem7  26390  logimcl  26611  qrngdiv  27665  etaslts  27863  ax5seg  29085  uhgr2edg  29355  umgr2edgneu  29361  uspgr1ewop  29395  iswlkg  29760  wlkonwlk  29807  trlontrl  29855  upgrwlkdvspth  29885  pthonpth  29894  spthonpthon  29897  uhgrwkspth  29901  usgr2wlkspthlem1  29903  usgr2wlkspthlem2  29904  usgr2wlkspth  29905  2pthon3v  30089  umgr2wlk  30095  rusgrnumwwlkg  30125  clwwisshclwws  30163  clwwlknp  30185  clwwlkfo  30198  clwwlknwwlkncl  30201  1pthond  30292  uhgr3cyclex  30330  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  numclwwlk3  30533  ajfuni  31008  funadj  32035  trleile  33110  isinftm  33322  bnj1098  35043  bnj546  35155  bnj998  35216  bnj1006  35219  bnj1173  35261  bnj1189  35268  onvfowev  35423  cusgr3cyclex  35450  elnanelprv  35743  cgr3permute1  36362  cgr3com  36367  brifs2  36392  idinside  36398  btwnconn1  36415  lineunray  36461  wl-nfeqfb  38003  dmqsblocks  39430  riotasv2s  39546  lsatlspsn2  39580  3dim2  40056  paddasslem14  40421  4atexlemex6  40662  cdlemg10bALTN  41224  cdlemg44  41321  tendoplcl  41369  hdmap14lem14  42469  nnawordexg  43868  pm13.194  44952  fmulcl  46121  fmuldfeqlem1  46122  stoweidlem17  46555  stoweidlem31  46569  dfsalgen2  46879  sigaraf  47391  sigarmf  47392  elfzelfzlble  47879  nprmmul2  48098  dfclnbgr6  48442  dfnbgr6  48443  dfsclnbgr6  48444  isubgr3stgrlem4  48555  funcringcsetcALTV2lem9  48884  funcringcsetclem9ALTV  48907  zlmodzxzscm  48943  divsub1dir  49103  elbigoimp  49142  digexp  49193  2arymptfv  49236  funcf2lem2  49667