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  1224  expdcom  1488  nebidc  2494  sbcimdv  3111  prel12  3880  reusv3  4586  relcoi1  5299  oprabid  6090  poxp  6441  reldmtpos  6497  tfrlem9  6563  tfri3  6611  ordiso2  7339  distrlem5prl  7917  distrlem5pru  7918  bndndx  9512  uzind2  9708  leexp1a  10980  swrdswrdlem  11421  swrdswrd  11422  swrdccat3blem  11456  reuccatpfxs1lem  11463  cncongr1  12825  infpnlem1  13082  gausslemma2dlem1a  16057  uhgr2edg  16327  bj-inf2vnlem2  16867