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

Theorem com3l 75
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 73 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com3r 73 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  78  imp3a  420  exp3acom3r  1370  prel12  3870  reusv3  4624  tfindsg  4733  sotri2  5154  relcoi1  5283  isofrlem  5924  oprabid  5969  frxp  6312  poxp  6314  reldmtpos  6329  sorpsscmpl  6375  tfrlem9  6488  tfr3  6502  oawordri  6635  odi  6664  omass  6665  undifixp  6940  isinf  7164  pssnn  7169  ordiso2  7320  ordtypelem7  7329  cantnf  7485  indcardi  7758  dfac2  7847  cfslb2n  7984  infpssrlem4  8022  axdc4lem  8171  zorn2lem7  8219  fpwwe2lem8  8349  grudomon  8529  distrlem5pr  8741  ltexprlem1  8750  axpre-sup  8881  bndndx  10056  uzind2  10196  difreicc  10859  leexp1a  11253  unbenlem  13052  infpnlem1  13054  neindisj2  16966  cmpsub  17233  grpomndo  21125  rngoueqz  21209  rngoridfz  21214  shscli  22010  mdbr3  22991  mdbr4  22992  dmdbr3  22999  dmdbr4  23000  mdslmd1i  23023  chjatom  23051  mdsymlem4  23100  cdj3lem2b  23131  3jaodd  24469  dfon2lem6  24702  poseq  24811  nocvxminlem  24902  funray  25322  imp5p  25544  brabg2  25690  neificl  25791  elfznelfzo  27462  usgrafisinds  27581  wlkdvspth  27744  usgrcyclnl2  27765  hashnbgravdg  27819  frgra3vlem1  27833  3vfriswmgralem  27837  vdn0frgrav2  27857  frgrawopreglem4  27880  eel32131  28247  bnj517  28679
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator