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  1228  expdcom  1492  nebidc  2500  sbcimdv  3117  prel12  3891  reusv3  4601  relcoi1  5314  oprabid  6107  poxp  6458  reldmtpos  6514  tfrlem9  6580  tfri3  6628  ordiso2  7365  distrlem5prl  7943  distrlem5pru  7944  bndndx  9541  uzind2  9737  leexp1a  11009  swrdswrdlem  11454  swrdswrd  11455  swrdccat3blem  11489  reuccatpfxs1lem  11496  cncongr1  12859  infpnlem1  13116  gausslemma2dlem1a  16091  uhgr2edg  16361  lealltlt1  16665  bj-inf2vnlem2  16911