Theorem 3simpc 1156

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adantl1  1173  3adantr1  1176  pr1eqbg  4795  fpropnf1  7218  fovcld  7490  find  7842  tz7.49c  8382  dif1en  9093  eqsup  9366  fimin2g  9409  mulcanenq  10881  elnpi  10909  divcan2  11815  divrec  11823  divcan3  11833  eliooord  13356  fzrev3  13542  modaddabs  13868  modaddmod  13869  muladdmodid  13870  modmulmod  13896  sqdiv  14081  swrdlend  14614  swrdnd  14615  ccats1pfxeqbi  14702  sqrmo  15211  muldvds2  16248  dvdscmul  16249  dvdsmulc  16250  dvdstr  16261  funcestrcsetclem9  18112  funcsetcestrclem9  18127  gsumccat  18807  domneq0  20687  znleval2  21537  redvr  21599  aspid  21856  scmatscmiddistr  22498  1marepvmarrepid  22565  mat2pmatghm  22720  pmatcollpw1lem1  22764  monmatcollpw  22769  pmatcollpwscmatlem2  22780  conncompss  23423  islly2  23474  elmptrab2  23818  tngngp3  24646  lmmcvg  25253  cmslsschl  25369  ivthicc  25450  aaliou3lem7  26340  logimcl  26558  qrngdiv  27612  etaslts  27810  ax5seg  29032  uhgr2edg  29302  umgr2edgneu  29308  uspgr1ewop  29342  iswlkg  29707  wlkonwlk  29754  trlontrl  29802  upgrwlkdvspth  29832  pthonpth  29841  spthonpthon  29844  uhgrwkspth  29848  usgr2wlkspthlem1  29850  usgr2wlkspthlem2  29851  usgr2wlkspth  29852  2pthon3v  30036  umgr2wlk  30042  rusgrnumwwlkg  30072  clwwisshclwws  30110  clwwlknp  30132  clwwlkfo  30145  clwwlknwwlkncl  30148  1pthond  30239  uhgr3cyclex  30277  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  numclwwlk3  30480  ajfuni  30955  funadj  31982  trleile  33057  isinftm  33269  bnj1098  34973  bnj546  35085  bnj998  35146  bnj1006  35149  bnj1173  35191  bnj1189  35198  cusgr3cyclex  35371  elnanelprv  35664  cgr3permute1  36283  cgr3com  36288  brifs2  36313  idinside  36319  btwnconn1  36336  lineunray  36382  wl-nfeqfb  37914  dmqsblocks  39341  riotasv2s  39457  lsatlspsn2  39491  3dim2  39967  paddasslem14  40332  4atexlemex6  40573  cdlemg10bALTN  41135  cdlemg44  41232  tendoplcl  41280  hdmap14lem14  42380  nnawordexg  43779  pm13.194  44863  fmulcl  46033  fmuldfeqlem1  46034  stoweidlem17  46467  stoweidlem31  46481  dfsalgen2  46791  sigaraf  47303  sigarmf  47304  elfzelfzlble  47791  nprmmul2  48010  dfclnbgr6  48354  dfnbgr6  48355  dfsclnbgr6  48356  isubgr3stgrlem4  48467  funcringcsetcALTV2lem9  48796  funcringcsetclem9ALTV  48819  zlmodzxzscm  48855  divsub1dir  49015  elbigoimp  49054  digexp  49105  2arymptfv  49148  funcf2lem2  49579