Theorem 3simpc 1150

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

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

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 1088

This theorem is referenced by:  3adantl1  1167  3adantr1  1170  pr1eqbg  4808  fpropnf1  7207  fovcld  7479  find  7831  tz7.49c  8371  dif1en  9078  eqsup  9347  fimin2g  9390  mulcanenq  10858  elnpi  10886  divcan2  11791  divrec  11799  divcan3  11809  eliooord  13307  fzrev3  13492  modaddabs  13817  modaddmod  13818  muladdmodid  13819  modmulmod  13845  sqdiv  14030  swrdlend  14563  swrdnd  14564  ccats1pfxeqbi  14651  sqrmo  15160  muldvds2  16194  dvdscmul  16195  dvdsmulc  16196  dvdstr  16207  funcestrcsetclem9  18056  funcsetcestrclem9  18071  gsumccat  18751  domneq0  20625  znleval2  21494  redvr  21556  aspid  21814  scmatscmiddistr  22424  1marepvmarrepid  22491  mat2pmatghm  22646  pmatcollpw1lem1  22690  monmatcollpw  22695  pmatcollpwscmatlem2  22706  conncompss  23349  islly2  23400  elmptrab2  23744  tngngp3  24572  lmmcvg  25189  cmslsschl  25305  ivthicc  25387  aaliou3lem7  26285  logimcl  26506  qrngdiv  27563  etasslt  27755  ax5seg  28918  uhgr2edg  29188  umgr2edgneu  29194  uspgr1ewop  29228  iswlkg  29594  wlkonwlk  29641  trlontrl  29689  upgrwlkdvspth  29719  pthonpth  29728  spthonpthon  29731  uhgrwkspth  29735  usgr2wlkspthlem1  29737  usgr2wlkspthlem2  29738  usgr2wlkspth  29739  2pthon3v  29923  umgr2wlk  29929  rusgrnumwwlkg  29959  clwwisshclwws  29997  clwwlknp  30019  clwwlkfo  30032  clwwlknwwlkncl  30035  1pthond  30126  uhgr3cyclex  30164  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  numclwwlk3  30367  ajfuni  30841  funadj  31868  trleile  32959  isinftm  33157  bnj1098  34816  bnj546  34929  bnj998  34990  bnj1006  34993  bnj1173  35035  bnj1189  35042  cusgr3cyclex  35201  elnanelprv  35494  cgr3permute1  36113  cgr3com  36118  brifs2  36143  idinside  36149  btwnconn1  36166  lineunray  36212  wl-nfeqfb  37601  dmqsblocks  38971  riotasv2s  39077  lsatlspsn2  39111  3dim2  39587  paddasslem14  39952  4atexlemex6  40193  cdlemg10bALTN  40755  cdlemg44  40852  tendoplcl  40900  hdmap14lem14  42000  nnawordexg  43444  pm13.194  44529  fmulcl  45705  fmuldfeqlem1  45706  stoweidlem17  46139  stoweidlem31  46153  dfsalgen2  46463  sigaraf  46975  sigarmf  46976  elfzelfzlble  47445  dfclnbgr6  47980  dfnbgr6  47981  dfsclnbgr6  47982  isubgr3stgrlem4  48093  funcringcsetcALTV2lem9  48422  funcringcsetclem9ALTV  48445  zlmodzxzscm  48481  divsub1dir  48642  elbigoimp  48681  digexp  48732  2arymptfv  48775  funcf2lem2  49207