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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adantl1  1185  3adantr1  1188  pr1eqbg  4823  fpropnf1  7267  fovcld  7539  find  7893  tz7.49c  8434  dif1en  9147  eqsup  9417  fimin2g  9460  mulcanenq  10946  elnpi  10974  divcan2  11881  divrec  11889  divcan3  11899  eliooord  13433  fzrev3  13620  modaddabs  13946  modaddmod  13947  muladdmodid  13948  modmulmod  13974  sqdiv  14159  swrdlend  14693  swrdnd  14694  ccats1pfxeqbi  14781  sqrmo  15304  muldvds2  16340  dvdscmul  16341  dvdsmulc  16342  dvdstr  16353  funcestrcsetclem9  18205  funcsetcestrclem9  18220  gsumccat  18901  rng1zr  20261  srg1zr  20298  domneq0  20794  znleval2  21686  redvr  21748  aspid  22005  scmatscmiddistr  22646  1marepvmarrepid  22713  mat2pmatghm  22868  pmatcollpw1lem1  22912  monmatcollpw  22917  pmatcollpwscmatlem2  22928  conncompss  23571  islly2  23622  elmptrab2  23966  tngngp3  24794  lmmcvg  25401  cmslsschl  25517  ivthicc  25598  aaliou3lem7  26491  logimcl  26712  qrngdiv  27766  etaslts  27964  ax5seg  29266  uhgr2edg  29536  umgr2edgneu  29542  uspgr1ewop  29576  iswlkg  29941  wlkonwlk  29988  trlontrl  30036  upgrwlkdvspth  30066  pthonpth  30075  spthonpthon  30078  uhgrwkspth  30082  usgr2wlkspthlem1  30084  usgr2wlkspthlem2  30085  usgr2wlkspth  30086  2pthon3v  30270  umgr2wlk  30276  rusgrnumwwlkg  30306  clwwisshclwws  30344  clwwlknp  30366  clwwlkfo  30379  clwwlknwwlkncl  30382  1pthond  30473  uhgr3cyclex  30511  numclwlk2lem2f  30706  numclwlk2lem2f1o  30708  numclwwlk3  30714  ajfuni  31189  funadj  32216  trleile  33269  isinftm  33479  bnj1098  35150  bnj546  35262  bnj998  35323  bnj1006  35326  bnj1173  35368  bnj1189  35375  onvfowev  35578  cusgr3cyclex  35606  elnanelprv  35899  cgr3permute1  36518  cgr3com  36523  brifs2  36548  idinside  36554  btwnconn1  36571  lineunray  36617  wl-nfeqfb  38169  dmqsblocks  39594  riotasv2s  39710  lsatlspsn2  39744  3dim2  40220  paddasslem14  40585  4atexlemex6  40826  cdlemg10bALTN  41388  cdlemg44  41485  tendoplcl  41533  hdmap14lem14  42633  nnawordexg  44034  pm13.194  45102  fmulcl  46277  fmuldfeqlem1  46278  stoweidlem17  46711  stoweidlem31  46725  dfsalgen2  47035  sigaraf  47547  sigarmf  47548  elfzelfzlble  48035  nprmmul2  48254  dfclnbgr6  48598  dfnbgr6  48599  dfsclnbgr6  48600  isubgr3stgrlem4  48711  funcringcsetcALTV2lem9  49040  funcringcsetclem9ALTV  49063  zlmodzxzscm  49114  divsub1dir  49274  elbigoimp  49313  digexp  49364  2arymptfv  49407  funcf2lem2  49837