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

Theorem com34 79
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 78 . 2  |-  ( ( ch  ->  ( th  ->  ta ) )  -> 
( th  ->  ( ch  ->  ta ) ) )
31, 2syl6 31 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  80  com35  86  3an1rs  1165  rspct  3037  po2nr  4508  wefrc  4568  tz7.7  4599  onint  4767  funssres  5485  isomin  6049  f1oweALT  6066  f1ocnv2d  6287  tfrlem9  6638  tz7.49  6694  oelim  6770  oaordex  6793  omordi  6801  omass  6815  oen0  6821  nnmass  6859  nnmordi  6866  inf3lem2  7574  epfrs  7657  indcardi  7912  ackbij1lem16  8105  cfcoflem  8142  axcc3  8308  zorn2lem7  8372  grur1a  8684  genpcd  8873  genpnmax  8874  mulclprlem  8886  distrlem1pr  8892  ltaddpr  8901  ltexprlem6  8908  ltexprlem7  8909  mulgt0sr  8970  divgt0  9868  divge0  9869  sup2  9954  uzind2  10352  uzwo  10529  uzwoOLD  10530  supxrun  10884  expnbnd  11498  facdiv  11568  caubnd  12152  joinle  14440  lmodvsdi  15963  xrsdsreclblem  16734  riinopn  16971  0ntr  17125  elcls  17127  hausnei2  17407  fgfil  17897  alexsubALTlem2  18069  alexsubALT  18072  aalioulem3  20241  aalioulem4  20242  wilthlem3  20843  grpoidinvlem3  21784  elspansn5  23066  atcv1  23873  atcvatlem  23878  chirredlem3  23885  mdsymlem3  23898  mdsymlem5  23900  mdsymlem6  23901  sumdmdlem2  23912  f1o3d  24031  wfrlem12  25534  frrlem11  25559  nndivsub  26172  mblfinlem2  26208  fgmin  26353  rngonegrmul  26522  crngm23  26566  psgnunilem4  27352  hashimarni  28106  swrdswrdlem  28128  2cshw2lem3  28184  cshwssizelem3  28209  usgra2adedgspthlem2  28231  3cyclfrgrarn  28304  n4cyclfrgra  28309  ad5ant14  28449  ad5ant15  28450  ad5ant24  28452  ad5ant25  28453  ad5ant245  28454  ad5ant124  28458  ad5ant134  28460  ad5ant135  28461  ad5ant145  28462  syl5imp  28496  com3rgbi  28498  ee223  28636  hlrelat2  30101  pmaple  30459  pmodlem2  30545  dalaw  30584
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator