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  4827  fpropnf1  7272  fovcld  7550  find  7901  tz7.49c  8442  dif1en  9156  eqsup  9426  fimin2g  9469  mulcanenq  10963  elnpi  10991  divcan2  11898  divrec  11906  divcan3  11916  eliooord  13450  fzrev3  13637  modaddabs  13964  modaddmod  13965  muladdmodid  13966  modmulmod  13992  sqdiv  14177  swrdlend  14715  swrdnd  14716  ccats1pfxeqbi  14803  sqrmo  15328  muldvds2  16364  dvdscmul  16365  dvdsmulc  16366  dvdstr  16377  funcestrcsetclem9  18229  funcsetcestrclem9  18244  gsumccat  18931  rng1zr  20291  srg1zr  20328  domneq0  20844  znleval2  21742  redvr  21804  aspid  22061  scmatscmiddistr  22702  1marepvmarrepid  22769  mat2pmatghm  22924  pmatcollpw1lem1  22968  monmatcollpw  22973  pmatcollpwscmatlem2  22984  conncompss  23627  islly2  23678  elmptrab2  24022  tngngp3  24850  lmmcvg  25457  cmslsschl  25573  ivthicc  25654  aaliou3lem7  26549  logimcl  26771  qrngdiv  27825  etaslts  28023  ax5seg  29325  uhgr2edg  29595  umgr2edgneu  29601  uspgr1ewop  29635  iswlkg  30000  wlkonwlk  30047  trlontrl  30095  upgrwlkdvspth  30125  pthonpth  30134  spthonpthon  30137  uhgrwkspth  30141  usgr2wlkspthlem1  30143  usgr2wlkspthlem2  30144  usgr2wlkspth  30145  2pthon3v  30329  umgr2wlk  30335  rusgrnumwwlkg  30365  clwwisshclwws  30403  clwwlknp  30425  clwwlkfo  30438  clwwlknwwlkncl  30441  1pthond  30532  uhgr3cyclex  30570  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  numclwwlk3  30773  ajfuni  31248  funadj  32275  trleile  33322  isinftm  33532  bnj1098  35204  bnj546  35316  bnj998  35377  bnj1006  35380  bnj1173  35422  bnj1189  35429  onvfowev  35624  cusgr3cyclex  35649  elnanelprv  35942  cgr3permute1  36561  cgr3com  36566  brifs2  36591  idinside  36597  btwnconn1  36614  lineunray  36660  wl-nfeqfb  38232  dmqsblocks  39657  riotasv2s  39773  lsatlspsn2  39807  3dim2  40283  paddasslem14  40648  4atexlemex6  40889  cdlemg10bALTN  41451  cdlemg44  41548  tendoplcl  41596  hdmap14lem14  42696  nnawordexg  44095  pm13.194  45163  fmulcl  46338  fmuldfeqlem1  46339  stoweidlem17  46772  stoweidlem31  46786  dfsalgen2  47096  sigaraf  47608  sigarmf  47609  elfzelfzlble  48099  nprmmul2  48318  dfclnbgr6  48662  dfnbgr6  48663  dfsclnbgr6  48664  isubgr3stgrlem4  48775  funcringcsetcALTV2lem9  49104  funcringcsetclem9ALTV  49127  zlmodzxzscm  49178  divsub1dir  49338  elbigoimp  49377  digexp  49428  2arymptfv  49471  funcf2lem2  49901