Theorem 3simpc 1147

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

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

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  3adantl1  1163  3adantr1  1166  pr1eqbg  4852  fpropnf1  7262  fovcld  7532  find  7884  findOLD  7885  tz7.49c  8447  dif1en  9162  eqsup  9453  fimin2g  9494  mulcanenq  10957  elnpi  10985  divcan2  11884  diveq0  11886  divrec  11892  divcan3  11902  eliooord  13389  fzrev3  13573  modaddabs  13880  modaddmod  13881  muladdmodid  13882  modmulmod  13907  sqdiv  14091  swrdlend  14609  swrdnd  14610  ccats1pfxeqbi  14698  sqrmo  15204  muldvds2  16232  dvdscmul  16233  dvdsmulc  16234  dvdstr  16244  funcestrcsetclem9  18112  funcsetcestrclem9  18127  gsumccat  18766  domneq0  21207  znleval2  21450  redvr  21510  aspid  21769  scmatscmiddistr  22365  1marepvmarrepid  22432  mat2pmatghm  22587  pmatcollpw1lem1  22631  monmatcollpw  22636  pmatcollpwscmatlem2  22647  conncompss  23292  islly2  23343  elmptrab2  23687  tngngp3  24528  lmmcvg  25144  cmslsschl  25260  ivthicc  25342  aaliou3lem7  26239  logimcl  26458  qrngdiv  27512  etasslt  27701  ax5seg  28704  uhgr2edg  28973  umgr2edgneu  28979  uspgr1ewop  29013  iswlkg  29379  wlkonwlk  29428  trlontrl  29477  upgrwlkdvspth  29505  pthonpth  29514  spthonpthon  29517  uhgrwkspth  29521  usgr2wlkspthlem1  29523  usgr2wlkspthlem2  29524  usgr2wlkspth  29525  2pthon3v  29706  umgr2wlk  29712  rusgrnumwwlkg  29739  clwwisshclwws  29777  clwwlknp  29799  clwwlkfo  29812  clwwlknwwlkncl  29815  1pthond  29906  uhgr3cyclex  29944  numclwlk2lem2f  30139  numclwlk2lem2f1o  30141  numclwwlk3  30147  ajfuni  30621  funadj  31648  trleile  32646  isinftm  32833  bnj1098  34323  bnj546  34436  bnj998  34497  bnj1006  34500  bnj1173  34542  bnj1189  34549  cusgr3cyclex  34655  elnanelprv  34948  cgr3permute1  35553  cgr3com  35558  brifs2  35583  idinside  35589  btwnconn1  35606  lineunray  35652  wl-nfeqfb  36912  riotasv2s  38341  lsatlspsn2  38375  3dim2  38852  paddasslem14  39217  4atexlemex6  39458  cdlemg10bALTN  40020  cdlemg44  40117  tendoplcl  40165  hdmap14lem14  41265  nnawordexg  42658  pm13.194  43752  fmulcl  44874  fmuldfeqlem1  44875  stoweidlem17  45310  stoweidlem31  45324  dfsalgen2  45634  sigaraf  46146  sigarmf  46147  elfzelfzlble  46606  funcringcsetcALTV2lem9  47253  funcringcsetclem9ALTV  47276  zlmodzxzscm  47314  divsub1dir  47478  elbigoimp  47522  digexp  47573  2arymptfv  47616