Theorem com3l 81

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 79	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com3r 79	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  84  impd  254  3imp231  1199  expdcom  1453  nebidc  2444  sbcimdv  3052  prel12  3798  reusv3  4492  relcoi1  5198  oprabid  5951  poxp  6287  reldmtpos  6308  tfrlem9  6374  tfri3  6422  ordiso2  7096  distrlem5prl  7648  distrlem5pru  7649  bndndx  9242  uzind2  9432  leexp1a  10668  cncongr1  12244  infpnlem1  12500  gausslemma2dlem1a  15215  bj-inf2vnlem2  15533