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  4801  fpropnf1  7215  fovcld  7487  find  7839  tz7.49c  8378  dif1en  9089  eqsup  9362  fimin2g  9405  mulcanenq  10874  elnpi  10902  divcan2  11808  divrec  11816  divcan3  11826  eliooord  13349  fzrev3  13535  modaddabs  13861  modaddmod  13862  muladdmodid  13863  modmulmod  13889  sqdiv  14074  swrdlend  14607  swrdnd  14608  ccats1pfxeqbi  14695  sqrmo  15204  muldvds2  16241  dvdscmul  16242  dvdsmulc  16243  dvdstr  16254  funcestrcsetclem9  18105  funcsetcestrclem9  18120  gsumccat  18800  domneq0  20676  znleval2  21545  redvr  21607  aspid  21864  scmatscmiddistr  22483  1marepvmarrepid  22550  mat2pmatghm  22705  pmatcollpw1lem1  22749  monmatcollpw  22754  pmatcollpwscmatlem2  22765  conncompss  23408  islly2  23459  elmptrab2  23803  tngngp3  24631  lmmcvg  25238  cmslsschl  25354  ivthicc  25435  aaliou3lem7  26326  logimcl  26546  qrngdiv  27601  etaslts  27799  ax5seg  29021  uhgr2edg  29291  umgr2edgneu  29297  uspgr1ewop  29331  iswlkg  29697  wlkonwlk  29744  trlontrl  29792  upgrwlkdvspth  29822  pthonpth  29831  spthonpthon  29834  uhgrwkspth  29838  usgr2wlkspthlem1  29840  usgr2wlkspthlem2  29841  usgr2wlkspth  29842  2pthon3v  30026  umgr2wlk  30032  rusgrnumwwlkg  30062  clwwisshclwws  30100  clwwlknp  30122  clwwlkfo  30135  clwwlknwwlkncl  30138  1pthond  30229  uhgr3cyclex  30267  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  numclwwlk3  30470  ajfuni  30945  funadj  31972  trleile  33046  isinftm  33257  bnj1098  34942  bnj546  35054  bnj998  35115  bnj1006  35118  bnj1173  35160  bnj1189  35167  cusgr3cyclex  35334  elnanelprv  35627  cgr3permute1  36246  cgr3com  36251  brifs2  36276  idinside  36282  btwnconn1  36299  lineunray  36345  wl-nfeqfb  37875  dmqsblocks  39302  riotasv2s  39418  lsatlspsn2  39452  3dim2  39928  paddasslem14  40293  4atexlemex6  40534  cdlemg10bALTN  41096  cdlemg44  41193  tendoplcl  41241  hdmap14lem14  42341  nnawordexg  43773  pm13.194  44857  fmulcl  46029  fmuldfeqlem1  46030  stoweidlem17  46463  stoweidlem31  46477  dfsalgen2  46787  sigaraf  47299  sigarmf  47300  elfzelfzlble  47781  nprmmul2  48000  dfclnbgr6  48344  dfnbgr6  48345  dfsclnbgr6  48346  isubgr3stgrlem4  48457  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809  zlmodzxzscm  48845  divsub1dir  49005  elbigoimp  49044  digexp  49095  2arymptfv  49138  funcf2lem2  49569