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

Theorem com3l 78
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 76 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com3r 76 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  81  imp3a  422  exp3acom3r  1380  prel12  3999  reusv3  4760  tfindsg  4869  sotri2  5292  relcoi1  5427  isofrlem  6089  oprabid  6134  frxp  6485  poxp  6487  reldmtpos  6516  sorpsscmpl  6562  tfrlem9  6675  tfr3  6689  oawordri  6822  odi  6851  omass  6852  undifixp  7127  isinf  7351  pssnn  7356  ordiso2  7513  ordtypelem7  7522  cantnf  7678  indcardi  7953  dfac2  8042  cfslb2n  8179  infpssrlem4  8217  axdc4lem  8366  zorn2lem7  8413  fpwwe2lem8  8543  grudomon  8723  distrlem5pr  8935  ltexprlem1  8944  axpre-sup  9075  bndndx  10251  uzind2  10393  difreicc  11059  elfznelfzo  11223  leexp1a  11469  unbenlem  13307  infpnlem1  13309  neindisj2  17218  cmpsub  17494  bwth  17504  usgrafisinds  21458  wlkdvspth  21639  usgrcyclnl2  21659  hashnbgravdg  21713  grpomndo  21965  rngoueqz  22049  rngoridfz  22054  shscli  22850  mdbr3  23831  mdbr4  23832  dmdbr3  23839  dmdbr4  23840  mdslmd1i  23863  chjatom  23891  mdsymlem4  23940  cdj3lem2b  23971  3jaodd  25199  dfon2lem6  25446  poseq  25559  nocvxminlem  25676  funray  26105  imp5p  26352  brabg2  26455  neificl  26497  uzletr  28150  subsubelfzo0  28182  fzoopth  28186  2ffzoeq  28187  swrdswrdlem  28256  swrdswrd  28257  swrdccat3blem  28276  2cshw1lem1  28306  usgra2pth  28373  el2spthonot  28426  2spontn0vne  28443  frgra3vlem1  28488  3vfriswmgralem  28492  vdn0frgrav2  28512  frgrawopreglem4  28534  eel12131  28919  eel32131  28922  3imp231  29028  bnj517  29354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator