Theorem 3simpc 1151

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adantl1  1168  3adantr1  1171  pr1eqbg  4800  fpropnf1  7222  fovcld  7494  find  7846  tz7.49c  8385  dif1en  9096  eqsup  9369  fimin2g  9412  mulcanenq  10883  elnpi  10911  divcan2  11817  divrec  11825  divcan3  11835  eliooord  13358  fzrev3  13544  modaddabs  13870  modaddmod  13871  muladdmodid  13872  modmulmod  13898  sqdiv  14083  swrdlend  14616  swrdnd  14617  ccats1pfxeqbi  14704  sqrmo  15213  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdstr  16263  funcestrcsetclem9  18114  funcsetcestrclem9  18129  gsumccat  18809  domneq0  20685  znleval2  21535  redvr  21597  aspid  21854  scmatscmiddistr  22473  1marepvmarrepid  22540  mat2pmatghm  22695  pmatcollpw1lem1  22739  monmatcollpw  22744  pmatcollpwscmatlem2  22755  conncompss  23398  islly2  23449  elmptrab2  23793  tngngp3  24621  lmmcvg  25228  cmslsschl  25344  ivthicc  25425  aaliou3lem7  26315  logimcl  26533  qrngdiv  27587  etaslts  27785  ax5seg  29007  uhgr2edg  29277  umgr2edgneu  29283  uspgr1ewop  29317  iswlkg  29682  wlkonwlk  29729  trlontrl  29777  upgrwlkdvspth  29807  pthonpth  29816  spthonpthon  29819  uhgrwkspth  29823  usgr2wlkspthlem1  29825  usgr2wlkspthlem2  29826  usgr2wlkspth  29827  2pthon3v  30011  umgr2wlk  30017  rusgrnumwwlkg  30047  clwwisshclwws  30085  clwwlknp  30107  clwwlkfo  30120  clwwlknwwlkncl  30123  1pthond  30214  uhgr3cyclex  30252  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  numclwwlk3  30455  ajfuni  30930  funadj  31957  trleile  33031  isinftm  33242  bnj1098  34926  bnj546  35038  bnj998  35099  bnj1006  35102  bnj1173  35144  bnj1189  35151  cusgr3cyclex  35318  elnanelprv  35611  cgr3permute1  36230  cgr3com  36235  brifs2  36260  idinside  36266  btwnconn1  36283  lineunray  36329  wl-nfeqfb  37861  dmqsblocks  39288  riotasv2s  39404  lsatlspsn2  39438  3dim2  39914  paddasslem14  40279  4atexlemex6  40520  cdlemg10bALTN  41082  cdlemg44  41179  tendoplcl  41227  hdmap14lem14  42327  nnawordexg  43755  pm13.194  44839  fmulcl  46011  fmuldfeqlem1  46012  stoweidlem17  46445  stoweidlem31  46459  dfsalgen2  46769  sigaraf  47281  sigarmf  47282  elfzelfzlble  47769  nprmmul2  47988  dfclnbgr6  48332  dfnbgr6  48333  dfsclnbgr6  48334  isubgr3stgrlem4  48445  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  zlmodzxzscm  48833  divsub1dir  48993  elbigoimp  49032  digexp  49083  2arymptfv  49126  funcf2lem2  49557