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  1221  expdcom  1485  nebidc  2480  sbcimdv  3094  prel12  3848  reusv3  4550  relcoi1  5259  oprabid  6032  poxp  6376  reldmtpos  6397  tfrlem9  6463  tfri3  6511  ordiso2  7198  distrlem5prl  7769  distrlem5pru  7770  bndndx  9364  uzind2  9555  leexp1a  10811  swrdswrdlem  11231  swrdswrd  11232  swrdccat3blem  11266  reuccatpfxs1lem  11273  cncongr1  12620  infpnlem1  12877  gausslemma2dlem1a  15731  uhgr2edg  15998  bj-inf2vnlem2  16292