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  2447  sbcimdv  3055  prel12  3802  reusv3  4496  relcoi1  5202  oprabid  5957  poxp  6299  reldmtpos  6320  tfrlem9  6386  tfri3  6434  ordiso2  7110  distrlem5prl  7670  distrlem5pru  7671  bndndx  9265  uzind2  9455  leexp1a  10703  cncongr1  12296  infpnlem1  12553  gausslemma2dlem1a  15383  bj-inf2vnlem2  15701