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  4833  fpropnf1  7259  fovcld  7532  find  7889  tz7.49c  8458  dif1en  9172  eqsup  9466  fimin2g  9509  mulcanenq  10972  elnpi  11000  divcan2  11902  divrec  11910  divcan3  11920  eliooord  13420  fzrev3  13605  modaddabs  13924  modaddmod  13925  muladdmodid  13926  modmulmod  13952  sqdiv  14137  swrdlend  14669  swrdnd  14670  ccats1pfxeqbi  14758  sqrmo  15268  muldvds2  16299  dvdscmul  16300  dvdsmulc  16301  dvdstr  16311  funcestrcsetclem9  18158  funcsetcestrclem9  18173  gsumccat  18817  domneq0  20666  znleval2  21514  redvr  21575  aspid  21833  scmatscmiddistr  22444  1marepvmarrepid  22511  mat2pmatghm  22666  pmatcollpw1lem1  22710  monmatcollpw  22715  pmatcollpwscmatlem2  22726  conncompss  23369  islly2  23420  elmptrab2  23764  tngngp3  24593  lmmcvg  25211  cmslsschl  25327  ivthicc  25409  aaliou3lem7  26307  logimcl  26528  qrngdiv  27585  etasslt  27775  ax5seg  28863  uhgr2edg  29133  umgr2edgneu  29139  uspgr1ewop  29173  iswlkg  29539  wlkonwlk  29588  trlontrl  29637  upgrwlkdvspth  29667  pthonpth  29676  spthonpthon  29679  uhgrwkspth  29683  usgr2wlkspthlem1  29685  usgr2wlkspthlem2  29686  usgr2wlkspth  29687  2pthon3v  29871  umgr2wlk  29877  rusgrnumwwlkg  29904  clwwisshclwws  29942  clwwlknp  29964  clwwlkfo  29977  clwwlknwwlkncl  29980  1pthond  30071  uhgr3cyclex  30109  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  numclwwlk3  30312  ajfuni  30786  funadj  31813  trleile  32897  isinftm  33125  bnj1098  34760  bnj546  34873  bnj998  34934  bnj1006  34937  bnj1173  34979  bnj1189  34986  cusgr3cyclex  35104  elnanelprv  35397  cgr3permute1  36012  cgr3com  36017  brifs2  36042  idinside  36048  btwnconn1  36065  lineunray  36111  wl-nfeqfb  37500  riotasv2s  38922  lsatlspsn2  38956  3dim2  39433  paddasslem14  39798  4atexlemex6  40039  cdlemg10bALTN  40601  cdlemg44  40698  tendoplcl  40746  hdmap14lem14  41846  nnawordexg  43298  pm13.194  44384  fmulcl  45558  fmuldfeqlem1  45559  stoweidlem17  45994  stoweidlem31  46008  dfsalgen2  46318  sigaraf  46830  sigarmf  46831  elfzelfzlble  47298  dfclnbgr6  47817  dfnbgr6  47818  dfsclnbgr6  47819  isubgr3stgrlem4  47929  funcringcsetcALTV2lem9  48221  funcringcsetclem9ALTV  48244  zlmodzxzscm  48280  divsub1dir  48441  elbigoimp  48484  digexp  48535  2arymptfv  48578  funcf2lem2  48995