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 769  prel12 2481  ordsssuc2 3055  tfindsg 3158  fvco2 3770  isofrlem 3896  tfrlem9 3914  tfr3 3921  oawordri 4177  odi 4203  omass 4204  pssnn 4522  rankr1 4657  aceq6b 4725  zorn2lem7 4777  unxpdomlem 4826  genpnmax 5093  ltexprlem1 5125  ssgt0sr 5200  nnleltp1t 5911  bndndx 6030  zneo 6157  zneoOLD 6158  uzind2 6164  mulexpt 6539  expaddt 6541  expmult 6542  expmwordit 6551  caucvglem2 7111  caucvglem4 7113  fsum0diag2 7211  unbenlem 7464  infpnlem1 7466  infxpidmlem7 7518  opnin 7831  metcn4i 7934  bcthlem28 7988  bcthlem29 7989  ubthlem10 8497  ubthlem11 8498  shscl 9236  5oalem6 9561  mdbr3 10180  mdbr4 10181  dmdbr3 10188  dmdbr4 10189  mdslmd1 10212  atom1d 10236  chjatom 10240  mdsymlem4 10289  cdj3lem2b 10320  uninqs 10400  fiv 10433  cdrci 10440  cnvhmpha 10471  cnvhmphb 10472  hmeogrp 10484  homcard 10485  filintf 10502  cnfilca 10510  mrdmcd 10638  cmpassoh 10645  cmpmon 10657  icmpmon 10659

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

Copyright terms: Public domain