Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpc Structured version   Visualization version   GIF version

Theorem 3simpc 1144
 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
StepHypRef Expression
1 id 22 . 2 ((𝜓𝜒) → (𝜓𝜒))
213adant1 1124 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1081 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 1083 This theorem is referenced by:  3adantl1  1160  3adantr1  1163  pr1eqbg  4786  fpropnf1  7021  find  7600  tz7.49c  8078  eqsup  8914  fimin2g  8955  mulcanenq  10376  elnpi  10404  divcan2  11300  diveq0  11302  divrec  11308  divcan3  11318  eliooord  12791  fzrev3  12968  modaddabs  13272  modaddmod  13273  muladdmodid  13274  modmulmod  13299  sqdiv  13482  swrdlend  14010  swrdnd  14011  ccats1pfxeqbi  14099  sqrmo  14606  muldvds2  15630  dvdscmul  15631  dvdsmulc  15632  dvdstr  15641  funcestrcsetclem9  17393  funcsetcestrclem9  17408  gsumccat  18001  domneq0  20005  aspid  20039  znleval2  20637  redvr  20696  scmatscmiddistr  21052  1marepvmarrepid  21119  mat2pmatghm  21273  pmatcollpw1lem1  21317  monmatcollpw  21322  pmatcollpwscmatlem2  21333  conncompss  21976  islly2  22027  elmptrab2  22371  tngngp3  23199  lmmcvg  23798  cmslsschl  23914  ivthicc  23993  aaliou3lem7  24872  logimcl  25085  qrngdiv  26133  ax5seg  26657  uhgr2edg  26923  umgr2edgneu  26929  uspgr1ewop  26963  iswlkg  27328  wlkonwlk  27377  trlontrl  27425  upgrwlkdvspth  27453  pthonpth  27462  spthonpthon  27465  uhgrwkspth  27469  usgr2wlkspthlem1  27471  usgr2wlkspthlem2  27472  usgr2wlkspth  27473  2pthon3v  27655  umgr2wlk  27661  rusgrnumwwlkg  27688  clwwisshclwws  27726  clwwlknp  27748  clwwlkfo  27762  clwwlknwwlkncl  27765  1pthond  27856  uhgr3cyclex  27894  numclwlk2lem2f  28089  numclwlk2lem2f1o  28091  numclwwlk3  28097  ajfuni  28569  funadj  29596  fovcld  30319  trleile  30586  isinftm  30743  bnj1098  31960  bnj546  32073  bnj998  32133  bnj1006  32136  bnj1173  32177  bnj1189  32184  cusgr3cyclex  32286  elnanelprv  32579  cgr3permute1  33412  cgr3com  33417  brifs2  33442  idinside  33448  btwnconn1  33465  lineunray  33511  wl-nfeqfb  34663  riotasv2s  35980  lsatlspsn2  36014  3dim2  36490  paddasslem14  36855  4atexlemex6  37096  cdlemg10bALTN  37658  cdlemg44  37755  tendoplcl  37803  hdmap14lem14  38903  pm13.194  40628  fmulcl  41746  fmuldfeqlem1  41747  stoweidlem17  42187  stoweidlem31  42201  dfsalgen2  42509  sigaraf  42995  sigarmf  42996  elfzelfzlble  43406  funcringcsetcALTV2lem9  44217  funcringcsetclem9ALTV  44240  zlmodzxzscm  44307  divsub1dir  44474  elbigoimp  44518  digexp  44569
 Copyright terms: Public domain W3C validator