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

Theorem com34 77
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 76 . 2  |-  ( ( ch  ->  ( th  ->  ta ) )  -> 
( th  ->  ( ch  ->  ta ) ) )
31, 2syl6 29 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  78  com35  84  3an1rs  1163  rspct  2877  po2nr  4327  wefrc  4387  tz7.7  4418  onint  4586  funssres  5294  isomin  5834  f1oweALT  5851  f1ocnv2d  6068  tfrlem9  6401  tz7.49  6457  oelim  6533  oaordex  6556  omordi  6564  omass  6578  oen0  6584  nnmass  6622  nnmordi  6629  inf3lem2  7330  epfrs  7413  indcardi  7668  ackbij1lem16  7861  cfcoflem  7898  axcc3  8064  zorn2lem7  8129  grur1a  8441  genpcd  8630  genpnmax  8631  mulclprlem  8643  distrlem1pr  8649  ltaddpr  8658  ltexprlem6  8665  ltexprlem7  8666  mulgt0sr  8727  divgt0  9624  divge0  9625  sup2  9710  uzind2  10104  uzwo  10281  uzwoOLD  10282  supxrun  10634  expnbnd  11230  facdiv  11300  caubnd  11842  joinle  14127  lmodvsdi  15650  xrsdsreclblem  16417  riinopn  16654  0ntr  16808  elcls  16810  hausnei2  17081  fgfil  17570  alexsubALTlem2  17742  alexsubALT  17745  aalioulem3  19714  aalioulem4  19715  wilthlem3  20308  grpoidinvlem3  20873  elspansn5  22153  atcv1  22960  atcvatlem  22965  chirredlem3  22972  mdsymlem3  22985  mdsymlem5  22987  mdsymlem6  22988  sumdmdlem2  22999  f1o3d  23037  wfrlem12  24267  frrlem11  24293  nndivsub  24896  prl  25167  ltrooo  25404  cmperltr  25409  glmrngo  25482  limptlimpr2lem2  25575  lvsovso2  25627  negveud  25668  negveudr  25669  cmpmon  25815  bsstr  26128  nbssntr  26129  lppotos  26144  bosser  26167  pdiveql  26168  fgmin  26319  rngonegrmul  26583  crngm23  26627  psgnunilem4  27420  syl5imp  28274  com3rgbi  28276  ee223  28406  hlrelat2  29592  pmaple  29950  pmodlem2  30036  dalaw  30075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator