Theorem com3l 80

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 78	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com3r 78	1 |- ( ps -> ( ch -> ( ph -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com4l  83  impd  251  expdcom  1371  nebidc  2325  sbcimdv  2879  prel12  3563  reusv3  4210  relcoi1  4869  oprabid  5557  poxp  5873  reldmtpos  5891  tfrlem9  5958  tfri3  5976  ordiso2  6446  distrlem5prl  6776  distrlem5pru  6777  bndndx  8287  uzind2  8459  leexp1a  9531  cncongr1  10485  bj-inf2vnlem2  10766