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

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
StepHypRef Expression
1 id 22 . 2 ((𝜓𝜒) → (𝜓𝜒))
213adant1 1125 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  simp3OLD  1151  3adant1OLD  1152  3adantl1  1172  3adantr1  1175  pr1eqbg  4534  fpropnf1  6688  find  7257  tz7.49c  7711  eqsup  8529  fimin2g  8570  mulcanenq  9994  elnpi  10022  divcan2  10905  diveq0  10907  divrec  10913  divcan3  10923  eliooord  12446  fzrev3  12619  modaddabs  12922  modaddmod  12923  muladdmodid  12924  modmulmod  12949  sqdiv  13142  swrdlend  13651  swrdnd  13652  ccats1swrdeqbi  13718  sqrmo  14211  muldvds2  15229  dvdscmul  15230  dvdsmulc  15231  dvdstr  15240  funcestrcsetclem9  17009  funcsetcestrclem9  17024  domneq0  19519  aspid  19552  znleval2  20126  redvr  20185  scmatscmiddistr  20536  1marepvmarrepid  20603  mat2pmatghm  20757  pmatcollpw1lem1  20801  monmatcollpw  20806  pmatcollpwscmatlem2  20817  conncompss  21458  islly2  21509  elmptrab2  21853  tngngp3  22681  lmmcvg  23279  ivthicc  23447  aaliou3lem7  24323  logimcl  24536  qrngdiv  25533  ax5seg  26038  uhgr2edg  26320  umgr2edgneu  26326  uspgr1ewop  26360  iswlkg  26740  wlkonprop  26785  wlkonwlk  26789  trlsonprop  26835  trlontrl  26838  upgrwlkdvspth  26866  pthsonprop  26871  spthonprop  26872  pthonpth  26875  spthonpthon  26878  uhgrwkspth  26882  usgr2wlkspthlem1  26884  usgr2wlkspthlem2  26885  usgr2wlkspth  26886  wwlknbp2OLD  26970  2pthon3v  27084  umgr2wlk  27090  rusgrnumwwlkg  27119  clwwisshclwws  27159  clwwlknp  27186  clwwlkfo  27200  clwwlknwwlkncl  27203  clwwlknwwlknclOLD  27204  clwlksfclwwlkOLD  27237  clwlksf1clwwlklemOLD  27243  1pthond  27317  uhgr3cyclex  27355  numclwlk2lem2f  27559  numclwlk2lem2f1o  27561  numclwlk2lem2fOLD  27566  numclwlk2lem2f1oOLD  27568  numclwwlk3  27574  ajfuni  28045  funadj  29075  fovcld  29770  trleile  29996  isinftm  30065  bnj1098  31182  bnj546  31294  bnj998  31354  bnj1006  31357  bnj1173  31398  bnj1189  31405  cgr3permute1  32482  cgr3com  32487  brifs2  32512  idinside  32518  btwnconn1  32535  lineunray  32581  wl-nfeqfb  33654  riotasv2s  34765  lsatlspsn2  34800  3dim2  35275  paddasslem14  35640  4atexlemex6  35881  cdlemg10bALTN  36444  cdlemg44  36541  tendoplcl  36589  hdmap14lem14  37693  pm13.194  39133  fmulcl  40334  fmuldfeqlem1  40335  stoweidlem17  40755  stoweidlem31  40769  dfsalgen2  41080  sigaraf  41566  sigarmf  41567  elfzelfzlble  41859  ccats1pfxeqbi  41959  funcringcsetcALTV2lem9  42572  funcringcsetclem9ALTV  42595  zlmodzxzscm  42663  divsub1dir  42835  elbigoimp  42878  digexp  42929
  Copyright terms: Public domain W3C validator