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

Theorem 3simpc 1058
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3simpc ((𝜑𝜓𝜒) → (𝜓𝜒))

Proof of Theorem 3simpc
StepHypRef Expression
1 3anrot 1041 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
2 3simpa 1056 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒))
31, 2sylbi 207 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  simp3  1061  3adant1  1077  3adantl1  1215  3adantr1  1218  pr1eqbg  4358  fpropnf1  6478  find  7038  tz7.49c  7486  eqsup  8306  fimin2g  8347  mulcanenq  9726  elnpi  9754  divcan2  10637  diveq0  10639  divrec  10645  divcan3  10655  eliooord  12175  fzrev3  12348  modaddabs  12648  modaddmod  12649  muladdmodid  12650  modmulmod  12675  sqdiv  12868  swrdlend  13369  swrdnd  13370  ccats1swrdeqbi  13435  sqrmo  13926  muldvds2  14931  dvdscmul  14932  dvdsmulc  14933  dvdstr  14942  funcestrcsetclem9  16709  funcsetcestrclem9  16724  domneq0  19216  aspid  19249  znleval2  19823  redvr  19882  scmatscmiddistr  20233  1marepvmarrepid  20300  mat2pmatghm  20454  pmatcollpw1lem1  20498  monmatcollpw  20503  pmatcollpwscmatlem2  20514  conncompss  21146  islly2  21197  elmptrab2OLD  21541  elmptrab2  21542  tngngp3  22370  lmmcvg  22967  ivthicc  23134  aaliou3lem7  24008  logimcl  24220  qrngdiv  25213  ax5seg  25718  uhgr2edg  25993  umgr2edgneu  25999  uspgr1ewop  26033  iswlkg  26379  wlkonprop  26423  wlkonwlk  26427  trlsonprop  26473  trlontrl  26476  upgrwlkdvspth  26504  pthsonprop  26509  spthonprop  26510  pthonpth  26513  spthonpthon  26516  uhgrwkspth  26520  usgr2wlkspthlem1  26522  usgr2wlkspthlem2  26523  usgr2wlkspth  26524  2pthon3v  26708  umgr2wlk  26714  rusgrnumwwlkg  26738  clwwlksfo  26784  clwwlksnwwlkncl  26787  clwwisshclwws  26794  clwlksfclwwlk  26828  clwlksf1clwwlklem  26834  1pthond  26870  uhgr3cyclex  26908  numclwlk1lem2f1  27082  numclwlk2lem2f  27091  numclwwlk3  27097  ajfuni  27564  funadj  28594  fovcld  29282  trleile  29451  isinftm  29520  bnj1098  30562  bnj546  30674  bnj998  30734  bnj1006  30737  bnj1173  30778  bnj1189  30785  cgr3permute1  31797  cgr3com  31802  brifs2  31827  idinside  31833  btwnconn1  31850  lineunray  31896  wl-nfeqfb  32955  riotasv2s  33724  lsatlspsn2  33759  3dim2  34234  paddasslem14  34599  4atexlemex6  34840  cdlemg10bALTN  35404  cdlemg44  35501  tendoplcl  35549  hdmap14lem14  36653  pm13.194  38095  fmulcl  39217  fmuldfeqlem1  39218  stoweidlem17  39541  stoweidlem31  39555  dfsalgen2  39866  sigaraf  40346  sigarmf  40347  elfzelfzlble  40628  ccats1pfxeqbi  40730  funcringcsetcALTV2lem9  41332  funcringcsetclem9ALTV  41355  zlmodzxzscm  41423  divsub1dir  41595  elbigoimp  41642  digexp  41693
  Copyright terms: Public domain W3C validator