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  1223  expdcom  1487  nebidc  2482  sbcimdv  3097  prel12  3854  reusv3  4557  relcoi1  5268  oprabid  6050  poxp  6397  reldmtpos  6419  tfrlem9  6485  tfri3  6533  ordiso2  7234  distrlem5prl  7806  distrlem5pru  7807  bndndx  9401  uzind2  9592  leexp1a  10857  swrdswrdlem  11289  swrdswrd  11290  swrdccat3blem  11324  reuccatpfxs1lem  11331  cncongr1  12693  infpnlem1  12950  gausslemma2dlem1a  15806  uhgr2edg  16076  bj-inf2vnlem2  16617