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 1087

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 1089

This theorem is referenced by:  3adantl1  1166  3adantr1  1169  pr1eqbg  4881  fpropnf1  7304  fovcld  7577  find  7935  tz7.49c  8502  dif1en  9226  eqsup  9525  fimin2g  9566  mulcanenq  11029  elnpi  11057  divcan2  11957  divrec  11965  divcan3  11975  eliooord  13466  fzrev3  13650  modaddabs  13960  modaddmod  13961  muladdmodid  13962  modmulmod  13987  sqdiv  14171  swrdlend  14701  swrdnd  14702  ccats1pfxeqbi  14790  sqrmo  15300  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  dvdstr  16342  funcestrcsetclem9  18217  funcsetcestrclem9  18232  gsumccat  18876  domneq0  20730  znleval2  21597  redvr  21658  aspid  21918  scmatscmiddistr  22535  1marepvmarrepid  22602  mat2pmatghm  22757  pmatcollpw1lem1  22801  monmatcollpw  22806  pmatcollpwscmatlem2  22817  conncompss  23462  islly2  23513  elmptrab2  23857  tngngp3  24698  lmmcvg  25314  cmslsschl  25430  ivthicc  25512  aaliou3lem7  26409  logimcl  26629  qrngdiv  27686  etasslt  27876  ax5seg  28971  uhgr2edg  29243  umgr2edgneu  29249  uspgr1ewop  29283  iswlkg  29649  wlkonwlk  29698  trlontrl  29747  upgrwlkdvspth  29775  pthonpth  29784  spthonpthon  29787  uhgrwkspth  29791  usgr2wlkspthlem1  29793  usgr2wlkspthlem2  29794  usgr2wlkspth  29795  2pthon3v  29976  umgr2wlk  29982  rusgrnumwwlkg  30009  clwwisshclwws  30047  clwwlknp  30069  clwwlkfo  30082  clwwlknwwlkncl  30085  1pthond  30176  uhgr3cyclex  30214  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  numclwwlk3  30417  ajfuni  30891  funadj  31918  trleile  32944  isinftm  33161  bnj1098  34759  bnj546  34872  bnj998  34933  bnj1006  34936  bnj1173  34978  bnj1189  34985  cusgr3cyclex  35104  elnanelprv  35397  cgr3permute1  36012  cgr3com  36017  brifs2  36042  idinside  36048  btwnconn1  36065  lineunray  36111  wl-nfeqfb  37490  riotasv2s  38914  lsatlspsn2  38948  3dim2  39425  paddasslem14  39790  4atexlemex6  40031  cdlemg10bALTN  40593  cdlemg44  40690  tendoplcl  40738  hdmap14lem14  41838  nnawordexg  43289  pm13.194  44381  fmulcl  45502  fmuldfeqlem1  45503  stoweidlem17  45938  stoweidlem31  45952  dfsalgen2  46262  sigaraf  46774  sigarmf  46775  elfzelfzlble  47236  dfclnbgr6  47728  dfnbgr6  47729  dfsclnbgr6  47730  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  zlmodzxzscm  48082  divsub1dir  48246  elbigoimp  48290  digexp  48341  2arymptfv  48384