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

Theorem com13 74
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com13  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 73 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com23 72 1  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com24  81  an13s  778  an31s  781  meredith  1394  peano5  4679  funopg  5286  abianfp  6471  omordi  6564  omeulem1  6580  brecop  6751  isinf  7076  fiint  7133  carduni  7614  dfac5  7755  dfac2  7757  cofsmo  7895  cfcoflem  7898  domtriomlem  8068  axdc3lem2  8077  nqereu  8553  squeeze0  9659  zmax  10313  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  difreicc  10767  uzindi  11043  facwordi  11302  sqr2irr  12527  spwmo  14335  fbunfip  17564  grpomndo  21013  rngoueqz  21097  shmodsi  21968  kbass6  22701  mdsymlem6  22988  mdsymlem7  22989  cdj3lem2a  23016  cdj3lem3a  23019  predpo  24184  11st22nd  25045  prj1b  25079  prj3  25080  prl2  25169  domrancur1c  25202  dfps2  25289  reacomsmgrp2  25344  resgcom  25351  grpodlcan  25376  rngodmeqrn  25419  zerdivemp1  25436  rngoridfz  25437  svli2  25484  svs2  25487  cmptdst  25568  islimrs4  25582  bwt2  25592  iintlem1  25610  lvsovso2  25627  addcanrg  25667  cmpassoh  25801  ismonc  25814  cmpmon  25815  icmpmon  25816  isepic  25824  carinttar  25902  prismorcsetlemb  25913  clscnc  26010  pxysxy  26142  pdiveql  26168  zerdivemp1x  26586  psgnunilem4  27420  funressnfv  27991  funbrafv  28020  nbgra0nb  28144  nbcusgra  28159  uvtxnbgra  28165  cusgrauvtx  28168  frgra3vlem1  28178  3imp31  28333  tratrbVD  28637  2uasbanhVD  28687  elpcliN  30082
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator