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

Theorem 3simpc 1152
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 1132 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  3adantl1  1168  3adantr1  1171  pr1eqbg  4772  fpropnf1  7084  find  7679  findOLD  7680  tz7.49c  8187  eqsup  9077  fimin2g  9118  mulcanenq  10579  elnpi  10607  divcan2  11503  diveq0  11505  divrec  11511  divcan3  11521  eliooord  12999  fzrev3  13183  modaddabs  13487  modaddmod  13488  muladdmodid  13489  modmulmod  13514  sqdiv  13698  swrdlend  14223  swrdnd  14224  ccats1pfxeqbi  14312  sqrmo  14820  muldvds2  15848  dvdscmul  15849  dvdsmulc  15850  dvdstr  15860  funcestrcsetclem9  17660  funcsetcestrclem9  17675  gsumccat  18273  domneq0  20340  znleval2  20525  redvr  20584  aspid  20839  scmatscmiddistr  21410  1marepvmarrepid  21477  mat2pmatghm  21632  pmatcollpw1lem1  21676  monmatcollpw  21681  pmatcollpwscmatlem2  21692  conncompss  22335  islly2  22386  elmptrab2  22730  tngngp3  23559  lmmcvg  24163  cmslsschl  24279  ivthicc  24360  aaliou3lem7  25247  logimcl  25463  qrngdiv  26510  ax5seg  27034  uhgr2edg  27301  umgr2edgneu  27307  uspgr1ewop  27341  iswlkg  27706  wlkonwlk  27755  trlontrl  27803  upgrwlkdvspth  27831  pthonpth  27840  spthonpthon  27843  uhgrwkspth  27847  usgr2wlkspthlem1  27849  usgr2wlkspthlem2  27850  usgr2wlkspth  27851  2pthon3v  28032  umgr2wlk  28038  rusgrnumwwlkg  28065  clwwisshclwws  28103  clwwlknp  28125  clwwlkfo  28138  clwwlknwwlkncl  28141  1pthond  28232  uhgr3cyclex  28270  numclwlk2lem2f  28465  numclwlk2lem2f1o  28467  numclwwlk3  28473  ajfuni  28945  funadj  29972  fovcld  30699  trleile  30973  isinftm  31159  bnj1098  32481  bnj546  32594  bnj998  32655  bnj1006  32658  bnj1173  32700  bnj1189  32707  cusgr3cyclex  32816  elnanelprv  33109  etasslt  33749  cgr3permute1  34092  cgr3com  34097  brifs2  34122  idinside  34128  btwnconn1  34145  lineunray  34191  wl-nfeqfb  35437  riotasv2s  36714  lsatlspsn2  36748  3dim2  37224  paddasslem14  37589  4atexlemex6  37830  cdlemg10bALTN  38392  cdlemg44  38489  tendoplcl  38537  hdmap14lem14  39637  pm13.194  41711  fmulcl  42805  fmuldfeqlem1  42806  stoweidlem17  43241  stoweidlem31  43255  dfsalgen2  43563  sigaraf  44049  sigarmf  44050  elfzelfzlble  44494  funcringcsetcALTV2lem9  45283  funcringcsetclem9ALTV  45306  zlmodzxzscm  45374  divsub1dir  45539  elbigoimp  45583  digexp  45634  2arymptfv  45677
  Copyright terms: Public domain W3C validator