Theorem com3l 34

Description: Commutation of antecedents. Rotate left.

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	com23 32	. 2 |- (ph -> (ch -> (ps -> th)))
3	2	com13 33	1 |- (ps -> (ch -> (ph -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  com3r 35  com4l 39  prlem1 770  prel12 2484  ordsssuc2 3059  tfindsg 3162  fvco2 3775  isofrlem 3901  tfrlem9 3919  tfr3 3926  oawordri 4184  odi 4210  omass 4211  pssnn 4534  rankr1 4674  aceq6b 4742  zorn2lem7 4794  unxpdomlem 4843  genpnmax 5110  ltexprlem1 5142  ssgt0sr 5217  nnleltp1t 5954  bndndx 6073  zneo 6200  uzind2 6206  mulexpt 6594  expaddt 6596  expmult 6597  expmwordit 6606  caucvglem2 7158  caucvglem4 7160  fsum0diag2 7259  unbenlem 7504  infpnlem1 7506  infxpidmlem7 7558  opnin 7869  metcn4i 7972  bcthlem28 8026  bcthlem29 8027  ubthlem10 8538  ubthlem11 8539  shscl 9281  5oalem6 9604  mdbr3 10224  mdbr4 10225  dmdbr3 10232  dmdbr4 10233  mdslmd1 10256  atom1d 10280  chjatom 10284  mdsymlem4 10333  cdj3lem2b 10364  uninqs 10441  fiv 10482  fivOLD 10483  cdrci 10494  cnvhmpha 10525  cnvhmphb 10526  hmeogrp 10538  homcard 10539  filintf 10569  cnfilca 10583  cnfilcaOLD 10584  mrdmcd 10722  cmpassoh 10729  cmpmon 10743  icmpmon 10744

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

Copyright terms: Public domain