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  2483  sbcimdv  3098  prel12  3859  reusv3  4563  relcoi1  5275  oprabid  6060  poxp  6406  reldmtpos  6462  tfrlem9  6528  tfri3  6576  ordiso2  7277  distrlem5prl  7849  distrlem5pru  7850  bndndx  9443  uzind2  9636  leexp1a  10902  swrdswrdlem  11334  swrdswrd  11335  swrdccat3blem  11369  reuccatpfxs1lem  11376  cncongr1  12738  infpnlem1  12995  gausslemma2dlem1a  15860  uhgr2edg  16130  bj-inf2vnlem2  16670