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

Theorem com3l 77
Description: Commutation of antecedents. Rotate left. (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
com3l  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )

Proof of Theorem com3l
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 75 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com3r 75 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  80  imp3a  421  exp3acom3r  1376  prel12  3935  reusv3  4690  tfindsg  4799  sotri2  5222  relcoi1  5357  isofrlem  6019  oprabid  6064  frxp  6415  poxp  6417  reldmtpos  6446  sorpsscmpl  6492  tfrlem9  6605  tfr3  6619  oawordri  6752  odi  6781  omass  6782  undifixp  7057  isinf  7281  pssnn  7286  ordiso2  7440  ordtypelem7  7449  cantnf  7605  indcardi  7878  dfac2  7967  cfslb2n  8104  infpssrlem4  8142  axdc4lem  8291  zorn2lem7  8338  fpwwe2lem8  8468  grudomon  8648  distrlem5pr  8860  ltexprlem1  8869  axpre-sup  9000  bndndx  10176  uzind2  10318  difreicc  10984  elfznelfzo  11147  leexp1a  11393  unbenlem  13231  infpnlem1  13233  neindisj2  17142  cmpsub  17417  usgrafisinds  21380  wlkdvspth  21561  usgrcyclnl2  21581  hashnbgravdg  21635  grpomndo  21887  rngoueqz  21971  rngoridfz  21976  shscli  22772  mdbr3  23753  mdbr4  23754  dmdbr3  23761  dmdbr4  23762  mdslmd1i  23785  chjatom  23813  mdsymlem4  23862  cdj3lem2b  23893  3jaodd  25121  dfon2lem6  25358  poseq  25467  nocvxminlem  25558  funray  25978  imp5p  26204  brabg2  26307  neificl  26349  swrdswrdlem  28010  swrdswrd  28011  usgra2pth  28041  el2spthonot  28067  2spontn0vne  28084  frgra3vlem1  28104  3vfriswmgralem  28108  vdn0frgrav2  28128  frgrawopreglem4  28150  eel12131  28530  eel32131  28533  3imp231  28639  bnj517  28962
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator