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  3943  reusv3  4698  tfindsg  4807  sotri2  5230  relcoi1  5365  isofrlem  6027  oprabid  6072  frxp  6423  poxp  6425  reldmtpos  6454  sorpsscmpl  6500  tfrlem9  6613  tfr3  6627  oawordri  6760  odi  6789  omass  6790  undifixp  7065  isinf  7289  pssnn  7294  ordiso2  7448  ordtypelem7  7457  cantnf  7613  indcardi  7886  dfac2  7975  cfslb2n  8112  infpssrlem4  8150  axdc4lem  8299  zorn2lem7  8346  fpwwe2lem8  8476  grudomon  8656  distrlem5pr  8868  ltexprlem1  8877  axpre-sup  9008  bndndx  10184  uzind2  10326  difreicc  10992  elfznelfzo  11155  leexp1a  11401  unbenlem  13239  infpnlem1  13241  neindisj2  17150  cmpsub  17425  usgrafisinds  21388  wlkdvspth  21569  usgrcyclnl2  21589  hashnbgravdg  21643  grpomndo  21895  rngoueqz  21979  rngoridfz  21984  shscli  22780  mdbr3  23761  mdbr4  23762  dmdbr3  23769  dmdbr4  23770  mdslmd1i  23793  chjatom  23821  mdsymlem4  23870  cdj3lem2b  23901  3jaodd  25129  dfon2lem6  25366  poseq  25475  nocvxminlem  25566  funray  25986  imp5p  26212  brabg2  26315  neificl  26357  swrdswrdlem  28018  swrdswrd  28019  usgra2pth  28049  el2spthonot  28075  2spontn0vne  28092  frgra3vlem1  28112  3vfriswmgralem  28116  vdn0frgrav2  28136  frgrawopreglem4  28158  eel12131  28539  eel32131  28542  3imp231  28648  bnj517  28974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator