Theorem 3simpc 1168

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 23	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	3adant1 1148	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl1  1185  3adantr1  1188  pr1eqbg  4811  fpropnf1  7271  fovcld  7547  find  7907  tz7.49c  8459  dif1en  9180  eqsup  9451  fimin2g  9494  mulcanenq  11048  elnpi  11076  divcan2  11985  divrec  11993  divcan3  12003  eliooord  13539  fzrev3  13727  modaddabs  14054  modaddmod  14055  muladdmodid  14056  modmulmod  14082  sqdiv  14267  swrdlend  14807  swrdnd  14808  ccats1pfxeqbi  14895  sqrmo  15423  muldvds2  16456  dvdscmul  16457  dvdsmulc  16458  dvdstr  16469  funcestrcsetclem9  18327  funcsetcestrclem9  18342  gsumccat  19042  rng1zr  20409  srg1zr  20446  domneq0  20965  znleval2  21866  redvr  21928  aspid  22187  scmatscmiddistr  22828  1marepvmarrepid  22895  mat2pmatghm  23053  pmatcollpw1lem1  23097  monmatcollpw  23102  pmatcollpwscmatlem2  23113  conncompss  23756  islly2  23808  elmptrab2  24152  tngngp3  24980  lmmcvg  25587  cmslsschl  25703  ivthicc  25784  aaliou3lem7  26681  logimcl  26902  qrngdiv  27956  etaslts  28184  ax5seg  29521  uhgr2edg  29794  umgr2edgneu  29800  uspgr1ewop  29834  iswlkg  30199  wlkonwlk  30246  trlontrl  30298  upgrwlkdvspth  30330  pthonpth  30339  spthonpthon  30342  uhgrwkspth  30346  usgr2wlkspthlem1  30348  usgr2wlkspthlem2  30349  usgr2wlkspth  30350  2pthon3v  30537  umgr2wlk  30543  rusgrnumwwlkg  30573  clwwisshclwws  30611  clwwlknp  30633  clwwlkfo  30646  clwwlknwwlkncl  30649  1pthond  30740  uhgr3cyclex  30788  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  numclwwlk3  30991  ajfuni  31466  funadj  32493  trleile  33578  isinftm  33788  bnj1098  35460  bnj546  35572  bnj998  35633  bnj1006  35636  bnj1173  35678  bnj1189  35685  onvfowev  35969  cusgr3cyclex  35987  elnanelprv  36280  cgr3permute1  36905  cgr3com  36910  brifs2  36935  idinside  36941  btwnconn1  36958  lineunray  37004  wl-nfeqfb  38561  dmqsblocks  39992  riotasv2s  40108  lsatlspsn2  40142  3dim2  40618  paddasslem14  40983  4atexlemex6  41224  cdlemg10bALTN  41786  cdlemg44  41883  tendoplcl  41931  hdmap14lem14  43031  nnawordexg  44422  pm13.194  45489  fmulcl  46686  fmuldfeqlem1  46687  stoweidlem17  47120  stoweidlem31  47134  dfsalgen2  47444  sigaraf  47956  sigarmf  47957  elfzelfzlble  48484  nprmmul2  48703  dfclnbgr6  49047  dfnbgr6  49048  dfsclnbgr6  49049  isubgr3stgrlem4  49160  funcringcsetcALTV2lem9  49488  funcringcsetclem9ALTV  49511  zlmodzxzscm  49562  divsub1dir  49722  elbigoimp  49761  digexp  49812  2arymptfv  49855  elixpmpt  50097  funcf2lem2  50289