Theorem com3l 89

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

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3r 87	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com3r 87	1 |- ( ps -> ( ch -> ( ph -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4l  92  impd  447  expdcom  455  3imp231  1258  rexlimdv  3030  sbcimdv  3498  reusv1  4866  reusv2lem3  4871  reusv3  4876  funopsn  6413  isofrlem  6590  oprabid  6677  sorpsscmpl  6948  tfindsg  7060  frxp  7287  poxp  7289  reldmtpos  7360  tfrlem9  7481  tfr3  7495  odi  7659  omass  7660  isinf  8173  pssnn  8178  ordiso2  8420  ordtypelem7  8429  cantnf  8590  indcardi  8864  dfac2  8953  cfslb2n  9090  infpssrlem4  9128  axdc4lem  9277  zorn2lem7  9324  fpwwe2lem8  9459  grudomon  9639  distrlem5pr  9849  ltexprlem1  9858  axpre-sup  9990  bndndx  11291  uzind2  11470  difreicc  12304  elfznelfzo  12573  ssnn0fi  12784  leexp1a  12919  swrdswrdlem  13459  swrdswrd  13460  swrdccat3blem  13495  cncongr1  15381  prm23ge5  15520  unbenlem  15612  infpnlem1  15614  initoeu1  16661  termoeu1  16668  ring1ne0  18591  neindisj2  20927  cmpsub  21203  gausslemma2dlem1a  25090  uhgr2edg  26100  wlklenvclwlk  26551  upgrwlkdvdelem  26632  usgr2pth  26660  wwlksm1edg  26767  wspn0  26820  frgr3vlem1  27137  3vfriswmgrlem  27141  frgrwopreglem4a  27174  frgrwopreg  27187  shscli  28176  mdbr3  29156  mdbr4  29157  dmdbr3  29164  dmdbr4  29165  mdslmd1i  29188  chjatom  29216  mdsymlem4  29265  cdj3lem2b  29296  bnj517  30955  3jaodd  31595  dfon2lem6  31693  poseq  31750  nocvxminlem  31893  funray  32247  imp5p  32305  brabg2  33510  neificl  33549  grpomndo  33674  rngoueqz  33739  subsubelfzo0  41336  fzoopth  41337  2ffzoeq  41338  reuccatpfxs1lem  41433  ztprmneprm  42125