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  2492  sbcimdv  3108  prel12  3875  reusv3  4581  relcoi1  5294  oprabid  6082  poxp  6428  reldmtpos  6484  tfrlem9  6550  tfri3  6598  ordiso2  7326  distrlem5prl  7901  distrlem5pru  7902  bndndx  9495  uzind2  9690  leexp1a  10956  swrdswrdlem  11396  swrdswrd  11397  swrdccat3blem  11431  reuccatpfxs1lem  11438  cncongr1  12800  infpnlem1  13057  gausslemma2dlem1a  15931  uhgr2edg  16201  bj-inf2vnlem2  16741