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  1453  nebidc  2447  sbcimdv  3055  prel12  3801  reusv3  4495  relcoi1  5201  oprabid  5954  poxp  6290  reldmtpos  6311  tfrlem9  6377  tfri3  6425  ordiso2  7101  distrlem5prl  7653  distrlem5pru  7654  bndndx  9248  uzind2  9438  leexp1a  10686  cncongr1  12271  infpnlem1  12528  gausslemma2dlem1a  15299  bj-inf2vnlem2  15617