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  252  3imp231  1179  expdcom  1422  nebidc  2407  sbcimdv  3002  prel12  3734  reusv3  4418  relcoi1  5114  oprabid  5847  poxp  6173  reldmtpos  6194  tfrlem9  6260  tfri3  6308  ordiso2  6969  distrlem5prl  7489  distrlem5pru  7490  bndndx  9072  uzind2  9259  leexp1a  10456  cncongr1  11960  bj-inf2vnlem2  13506