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  1199  expdcom  1461  nebidc  2455  sbcimdv  3063  prel12  3811  reusv3  4506  relcoi1  5213  oprabid  5975  poxp  6317  reldmtpos  6338  tfrlem9  6404  tfri3  6452  ordiso2  7136  distrlem5prl  7698  distrlem5pru  7699  bndndx  9293  uzind2  9484  leexp1a  10737  cncongr1  12367  infpnlem1  12624  gausslemma2dlem1a  15477  bj-inf2vnlem2  15840