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  1200  expdcom  1463  nebidc  2457  sbcimdv  3068  prel12  3818  reusv3  4515  relcoi1  5223  oprabid  5989  poxp  6331  reldmtpos  6352  tfrlem9  6418  tfri3  6466  ordiso2  7152  distrlem5prl  7719  distrlem5pru  7720  bndndx  9314  uzind2  9505  leexp1a  10761  swrdswrdlem  11180  swrdswrd  11181  cncongr1  12500  infpnlem1  12757  gausslemma2dlem1a  15610  bj-inf2vnlem2  16045