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  2890  po2nr  4343  wefrc  4403  tz7.7  4434  onint  4602  funssres  5310  isomin  5850  f1oweALT  5867  f1ocnv2d  6084  tfrlem9  6417  tz7.49  6473  oelim  6549  oaordex  6572  omordi  6580  omass  6594  oen0  6600  nnmass  6638  nnmordi  6645  inf3lem2  7346  epfrs  7429  indcardi  7684  ackbij1lem16  7877  cfcoflem  7914  axcc3  8080  zorn2lem7  8145  grur1a  8457  genpcd  8646  genpnmax  8647  mulclprlem  8659  distrlem1pr  8665  ltaddpr  8674  ltexprlem6  8681  ltexprlem7  8682  mulgt0sr  8743  divgt0  9640  divge0  9641  sup2  9726  uzind2  10120  uzwo  10297  uzwoOLD  10298  supxrun  10650  expnbnd  11246  facdiv  11316  caubnd  11858  joinle  14143  lmodvsdi  15666  xrsdsreclblem  16433  riinopn  16670  0ntr  16824  elcls  16826  hausnei2  17097  fgfil  17586  alexsubALTlem2  17758  alexsubALT  17761  aalioulem3  19730  aalioulem4  19731  wilthlem3  20324  grpoidinvlem3  20889  elspansn5  22169  atcv1  22976  atcvatlem  22981  chirredlem3  22988  mdsymlem3  23001  mdsymlem5  23003  mdsymlem6  23004  sumdmdlem2  23015  f1o3d  23053  wfrlem12  24338  frrlem11  24364  nndivsub  24968  prl  25270  ltrooo  25507  cmperltr  25512  glmrngo  25585  limptlimpr2lem2  25678  lvsovso2  25730  negveud  25771  negveudr  25772  cmpmon  25918  bsstr  26231  nbssntr  26232  lppotos  26247  bosser  26270  pdiveql  26271  fgmin  26422  rngonegrmul  26686  crngm23  26730  psgnunilem4  27523  3cyclfrgrarn  28436  n4cyclfrgra  28440  ad5ant14  28529  ad5ant15  28530  ad5ant24  28532  ad5ant25  28533  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  ad5ant124  28538  ad5ant125  28539  ad5ant134  28540  ad5ant135  28541  ad5ant145  28542  syl5imp  28573  com3rgbi  28575  ee223  28711  eel32131  28801  hlrelat2  30214  pmaple  30572  pmodlem2  30658  dalaw  30697
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator