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  252  expdcom  1418  nebidc  2388  sbcimdv  2974  prel12  3698  reusv3  4381  relcoi1  5070  oprabid  5803  poxp  6129  reldmtpos  6150  tfrlem9  6216  tfri3  6264  ordiso2  6920  distrlem5prl  7394  distrlem5pru  7395  bndndx  8976  uzind2  9163  leexp1a  10348  cncongr1  11784  bj-inf2vnlem2  13169