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  4820  fpropnf1  7268  fovcld  7544  find  7896  tz7.49c  8439  dif1en  9160  eqsup  9430  fimin2g  9473  mulcanenq  10973  elnpi  11001  divcan2  11908  divrec  11916  divcan3  11926  eliooord  13462  fzrev3  13649  modaddabs  13976  modaddmod  13977  muladdmodid  13978  modmulmod  14004  sqdiv  14189  swrdlend  14727  swrdnd  14728  ccats1pfxeqbi  14815  sqrmo  15342  muldvds2  16377  dvdscmul  16378  dvdsmulc  16379  dvdstr  16390  funcestrcsetclem9  18242  funcsetcestrclem9  18257  gsumccat  18956  rng1zr  20323  srg1zr  20360  domneq0  20876  znleval2  21774  redvr  21836  aspid  22095  scmatscmiddistr  22736  1marepvmarrepid  22803  mat2pmatghm  22961  pmatcollpw1lem1  23005  monmatcollpw  23010  pmatcollpwscmatlem2  23021  conncompss  23664  islly2  23716  elmptrab2  24060  tngngp3  24888  lmmcvg  25495  cmslsschl  25611  ivthicc  25692  aaliou3lem7  26592  logimcl  26814  qrngdiv  27868  etaslts  28066  ax5seg  29403  uhgr2edg  29676  umgr2edgneu  29682  uspgr1ewop  29716  iswlkg  30081  wlkonwlk  30128  trlontrl  30180  upgrwlkdvspth  30212  pthonpth  30221  spthonpthon  30224  uhgrwkspth  30228  usgr2wlkspthlem1  30230  usgr2wlkspthlem2  30231  usgr2wlkspth  30232  2pthon3v  30419  umgr2wlk  30425  rusgrnumwwlkg  30455  clwwisshclwws  30493  clwwlknp  30515  clwwlkfo  30528  clwwlknwwlkncl  30531  1pthond  30622  uhgr3cyclex  30670  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  numclwwlk3  30873  ajfuni  31348  funadj  32375  trleile  33419  isinftm  33629  bnj1098  35301  bnj546  35413  bnj998  35474  bnj1006  35477  bnj1173  35519  bnj1189  35526  onvfowev  35721  cusgr3cyclex  35733  elnanelprv  36016  cgr3permute1  36636  cgr3com  36641  brifs2  36666  idinside  36672  btwnconn1  36689  lineunray  36735  wl-nfeqfb  38307  dmqsblocks  39723  riotasv2s  39839  lsatlspsn2  39873  3dim2  40349  paddasslem14  40714  4atexlemex6  40955  cdlemg10bALTN  41517  cdlemg44  41614  tendoplcl  41662  hdmap14lem14  42762  nnawordexg  44176  pm13.194  45244  fmulcl  46419  fmuldfeqlem1  46420  stoweidlem17  46853  stoweidlem31  46867  dfsalgen2  47177  sigaraf  47689  sigarmf  47690  elfzelfzlble  48217  nprmmul2  48436  dfclnbgr6  48780  dfnbgr6  48781  dfsclnbgr6  48782  isubgr3stgrlem4  48893  funcringcsetcALTV2lem9  49221  funcringcsetclem9ALTV  49244  zlmodzxzscm  49295  divsub1dir  49455  elbigoimp  49494  digexp  49545  2arymptfv  49588  funcf2lem2  50016