MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com34 Structured version   Unicode version

Theorem com34 86
Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com34  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )

Proof of Theorem com34
StepHypRef Expression
1 com4.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
2 pm2.04 85 . 2  |-  ( ( ch  ->  ( th  ->  ta ) )  -> 
( th  ->  ( ch  ->  ta ) ) )
31, 2syl6 34 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com4l  87  com35  93  3an1rs  1217  ad5ant14  1240  ad5ant15  1241  ad5ant24  1243  ad5ant25  1244  ad5ant245  1245  ad5ant124  1249  ad5ant134  1251  ad5ant135  1252  ad5ant145  1253  rspct  3175  po2nr  4784  wefrc  4844  tz7.7  5465  funssres  5638  isomin  6240  f1ocnv2d  6531  onint  6633  f1oweALT  6788  wfrlem12  7052  tfrlem9  7108  tz7.49  7167  oelim  7241  oaordex  7264  omordi  7272  omass  7286  oen0  7292  nnmass  7330  nnmordi  7337  inf3lem2  8137  epfrs  8217  indcardi  8473  ackbij1lem16  8666  cfcoflem  8703  axcc3  8869  zorn2lem7  8933  grur1a  9245  genpcd  9432  genpnmax  9433  mulclprlem  9445  distrlem1pr  9451  ltaddpr  9460  ltexprlem6  9467  ltexprlem7  9468  mulgt0sr  9530  divgt0  10474  divge0  10475  sup2  10566  uzind2  11029  uzwo  11223  supxrun  11602  expnbnd  12401  facdiv  12472  hashimarni  12609  swrdswrdlem  12806  wrd2ind  12825  caubnd  13410  lcmfunsnlem2lem1  14599  ncoprmlnprm  14665  cshwshashlem1  15054  psgnunilem4  17126  lmodvsdi  18102  xrsdsreclblem  19002  cpmatacl  19727  riinopn  19925  0ntr  20074  elcls  20076  hausnei2  20356  fgfil  20877  alexsubALTlem2  21050  alexsubALT  21053  aalioulem3  23277  aalioulem4  23278  wilthlem3  23982  usgra2adedgspthlem2  25326  nbhashuvtx1  25629  3cyclfrgrarn  25727  n4cyclfrgra  25732  frgraregord013  25832  grpoidinvlem3  25920  elspansn5  27213  atcv1  28019  atcvatlem  28024  chirredlem3  28031  mdsymlem3  28044  mdsymlem5  28046  mdsymlem6  28047  sumdmdlem2  28058  f1o3d  28219  slmdvsdi  28526  frrlem11  30521  fgmin  31019  nndivsub  31110  mblfinlem3  31893  rngonegrmul  32105  crngm23  32149  hlrelat2  32887  pmaple  33245  pmodlem2  33331  dalaw  33370  syl5imp  36727  com3rgbi  36729  ee223  36872  iccpartigtl  38449  iccelpart  38459  bgoldbtbndlem3  38614  nzerooringczr  39346  ply1mulgsumlem1  39452  fllog2  39653
  Copyright terms: Public domain W3C validator