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

Theorem 3simpc 1175
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 1153 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simp3OLD  1179  3adant1OLD  1180  3adantl1  1200  3adantr1  1203  pr1eqbg  4588  fpropnf1  6758  find  7331  tz7.49c  7787  eqsup  8611  fimin2g  8652  mulcanenq  10077  elnpi  10105  divcan2  10988  diveq0  10990  divrec  10996  divcan3  11006  eliooord  12471  fzrev3  12649  modaddabs  12952  modaddmod  12953  muladdmodid  12954  modmulmod  12979  sqdiv  13171  swrdlend  13675  swrdnd  13676  ccats1swrdeqbi  13742  sqrmo  14235  muldvds2  15250  dvdscmul  15251  dvdsmulc  15252  dvdstr  15261  funcestrcsetclem9  17013  funcsetcestrclem9  17028  domneq0  19526  aspid  19559  znleval2  20131  redvr  20192  scmatscmiddistr  20546  1marepvmarrepid  20613  mat2pmatghm  20769  pmatcollpw1lem1  20813  monmatcollpw  20818  pmatcollpwscmatlem2  20829  conncompss  21471  islly2  21522  elmptrab2  21866  tngngp3  22694  lmmcvg  23293  ivthicc  23462  aaliou3lem7  24341  logimcl  24553  qrngdiv  25550  ax5seg  26055  uhgr2edg  26338  umgr2edgneu  26344  uspgr1ewop  26379  iswlkg  26760  wlkonprop  26805  wlkonwlk  26809  trlsonprop  26855  trlontrl  26858  upgrwlkdvspth  26886  pthsonprop  26891  spthonprop  26892  pthonpth  26895  spthonpthon  26898  uhgrwkspth  26902  usgr2wlkspthlem1  26904  usgr2wlkspthlem2  26905  usgr2wlkspth  26906  wwlknbp2OLD  26990  2pthon3v  27106  umgr2wlk  27112  rusgrnumwwlkg  27141  clwwisshclwws  27181  clwwlknp  27208  clwwlkfo  27222  clwwlknwwlkncl  27225  clwwlknwwlknclOLD  27226  clwlksfclwwlkOLD  27259  clwlksf1clwwlklemOLD  27265  1pthond  27340  uhgr3cyclex  27378  numclwlk2lem2f  27580  numclwlk2lem2f1o  27582  numclwlk2lem2fOLD  27587  numclwlk2lem2f1oOLD  27589  numclwwlk3  27596  ajfuni  28066  funadj  29096  fovcld  29790  trleile  30014  isinftm  30083  bnj1098  31199  bnj546  31311  bnj998  31371  bnj1006  31374  bnj1173  31415  bnj1189  31422  cgr3permute1  32498  cgr3com  32503  brifs2  32528  idinside  32534  btwnconn1  32551  lineunray  32597  wl-nfeqfb  33656  riotasv2s  34756  lsatlspsn2  34791  3dim2  35267  paddasslem14  35632  4atexlemex6  35873  cdlemg10bALTN  36435  cdlemg44  36532  tendoplcl  36580  hdmap14lem14  37680  pm13.194  39130  fmulcl  40311  fmuldfeqlem1  40312  stoweidlem17  40731  stoweidlem31  40745  dfsalgen2  41056  sigaraf  41542  sigarmf  41543  elfzelfzlble  41924  ccats1pfxeqbi  42024  funcringcsetcALTV2lem9  42630  funcringcsetclem9ALTV  42653  zlmodzxzscm  42721  divsub1dir  42893  elbigoimp  42936  digexp  42987
  Copyright terms: Public domain W3C validator