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 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adantl1  1166  3adantr1  1169  pr1eqbg  4857  fpropnf1  7265  fovcld  7535  find  7886  findOLD  7887  tz7.49c  8445  dif1en  9159  eqsup  9450  fimin2g  9491  mulcanenq  10954  elnpi  10982  divcan2  11879  diveq0  11881  divrec  11887  divcan3  11897  eliooord  13382  fzrev3  13566  modaddabs  13873  modaddmod  13874  muladdmodid  13875  modmulmod  13900  sqdiv  14085  swrdlend  14602  swrdnd  14603  ccats1pfxeqbi  14691  sqrmo  15197  muldvds2  16224  dvdscmul  16225  dvdsmulc  16226  dvdstr  16236  funcestrcsetclem9  18099  funcsetcestrclem9  18114  gsumccat  18721  domneq0  20912  znleval2  21110  redvr  21169  aspid  21428  scmatscmiddistr  22009  1marepvmarrepid  22076  mat2pmatghm  22231  pmatcollpw1lem1  22275  monmatcollpw  22280  pmatcollpwscmatlem2  22291  conncompss  22936  islly2  22987  elmptrab2  23331  tngngp3  24172  lmmcvg  24777  cmslsschl  24893  ivthicc  24974  aaliou3lem7  25861  logimcl  26077  qrngdiv  27124  etasslt  27311  ax5seg  28193  uhgr2edg  28462  umgr2edgneu  28468  uspgr1ewop  28502  iswlkg  28867  wlkonwlk  28916  trlontrl  28965  upgrwlkdvspth  28993  pthonpth  29002  spthonpthon  29005  uhgrwkspth  29009  usgr2wlkspthlem1  29011  usgr2wlkspthlem2  29012  usgr2wlkspth  29013  2pthon3v  29194  umgr2wlk  29200  rusgrnumwwlkg  29227  clwwisshclwws  29265  clwwlknp  29287  clwwlkfo  29300  clwwlknwwlkncl  29303  1pthond  29394  uhgr3cyclex  29432  numclwlk2lem2f  29627  numclwlk2lem2f1o  29629  numclwwlk3  29635  ajfuni  30107  funadj  31134  trleile  32136  isinftm  32322  bnj1098  33789  bnj546  33902  bnj998  33963  bnj1006  33966  bnj1173  34008  bnj1189  34015  cusgr3cyclex  34122  elnanelprv  34415  cgr3permute1  35015  cgr3com  35020  brifs2  35045  idinside  35051  btwnconn1  35068  lineunray  35114  wl-nfeqfb  36400  riotasv2s  37823  lsatlspsn2  37857  3dim2  38334  paddasslem14  38699  4atexlemex6  38940  cdlemg10bALTN  39502  cdlemg44  39599  tendoplcl  39647  hdmap14lem14  40747  nnawordexg  42067  pm13.194  43161  fmulcl  44287  fmuldfeqlem1  44288  stoweidlem17  44723  stoweidlem31  44737  dfsalgen2  45047  sigaraf  45559  sigarmf  45560  elfzelfzlble  46019  funcringcsetcALTV2lem9  46932  funcringcsetclem9ALTV  46955  zlmodzxzscm  47023  divsub1dir  47188  elbigoimp  47232  digexp  47283  2arymptfv  47326