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  4817  fpropnf1  7263  fovcld  7539  find  7896  tz7.49c  8440  dif1en  9161  eqsup  9432  fimin2g  9475  mulcanenq  11026  elnpi  11054  divcan2  11963  divrec  11971  divcan3  11981  eliooord  13517  fzrev3  13704  modaddabs  14031  modaddmod  14032  muladdmodid  14033  modmulmod  14059  sqdiv  14244  swrdlend  14783  swrdnd  14784  ccats1pfxeqbi  14871  sqrmo  15398  muldvds2  16431  dvdscmul  16432  dvdsmulc  16433  dvdstr  16444  funcestrcsetclem9  18302  funcsetcestrclem9  18317  gsumccat  19017  rng1zr  20384  srg1zr  20421  domneq0  20940  znleval2  21841  redvr  21903  aspid  22162  scmatscmiddistr  22803  1marepvmarrepid  22870  mat2pmatghm  23028  pmatcollpw1lem1  23072  monmatcollpw  23077  pmatcollpwscmatlem2  23088  conncompss  23731  islly2  23783  elmptrab2  24127  tngngp3  24955  lmmcvg  25562  cmslsschl  25678  ivthicc  25759  aaliou3lem7  26658  logimcl  26879  qrngdiv  27933  etaslts  28161  ax5seg  29498  uhgr2edg  29771  umgr2edgneu  29777  uspgr1ewop  29811  iswlkg  30176  wlkonwlk  30223  trlontrl  30275  upgrwlkdvspth  30307  pthonpth  30316  spthonpthon  30319  uhgrwkspth  30323  usgr2wlkspthlem1  30325  usgr2wlkspthlem2  30326  usgr2wlkspth  30327  2pthon3v  30514  umgr2wlk  30520  rusgrnumwwlkg  30550  clwwisshclwws  30588  clwwlknp  30610  clwwlkfo  30623  clwwlknwwlkncl  30626  1pthond  30717  uhgr3cyclex  30765  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  numclwwlk3  30968  ajfuni  31443  funadj  32470  trleile  33514  isinftm  33724  bnj1098  35397  bnj546  35509  bnj998  35570  bnj1006  35573  bnj1173  35615  bnj1189  35622  onvfowev  35868  cusgr3cyclex  35880  elnanelprv  36163  cgr3permute1  36783  cgr3com  36788  brifs2  36813  idinside  36819  btwnconn1  36836  lineunray  36882  wl-nfeqfb  38436  dmqsblocks  39867  riotasv2s  39983  lsatlspsn2  40017  3dim2  40493  paddasslem14  40858  4atexlemex6  41099  cdlemg10bALTN  41661  cdlemg44  41758  tendoplcl  41806  hdmap14lem14  42906  nnawordexg  44287  pm13.194  45355  fmulcl  46537  fmuldfeqlem1  46538  stoweidlem17  46971  stoweidlem31  46985  dfsalgen2  47295  sigaraf  47807  sigarmf  47808  elfzelfzlble  48335  nprmmul2  48554  dfclnbgr6  48898  dfnbgr6  48899  dfsclnbgr6  48900  isubgr3stgrlem4  49011  funcringcsetcALTV2lem9  49339  funcringcsetclem9ALTV  49362  zlmodzxzscm  49413  divsub1dir  49573  elbigoimp  49612  digexp  49663  2arymptfv  49706  funcf2lem2  50134