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  6049  poxp  6396  reldmtpos  6418  tfrlem9  6484  tfri3  6532  ordiso2  7233  distrlem5prl  7805  distrlem5pru  7806  bndndx  9400  uzind2  9591  leexp1a  10855  swrdswrdlem  11284  swrdswrd  11285  swrdccat3blem  11319  reuccatpfxs1lem  11326  cncongr1  12674  infpnlem1  12931  gausslemma2dlem1a  15786  uhgr2edg  16056  bj-inf2vnlem2  16566