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  3imp231  1192  expdcom  1435  nebidc  2420  sbcimdv  3020  prel12  3758  reusv3  4445  relcoi1  5142  oprabid  5885  poxp  6211  reldmtpos  6232  tfrlem9  6298  tfri3  6346  ordiso2  7012  distrlem5prl  7548  distrlem5pru  7549  bndndx  9134  uzind2  9324  leexp1a  10531  cncongr1  12057  infpnlem1  12311  bj-inf2vnlem2  14006