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  expdcom  1419  nebidc  2389  sbcimdv  2978  prel12  3706  reusv3  4389  relcoi1  5078  oprabid  5811  poxp  6137  reldmtpos  6158  tfrlem9  6224  tfri3  6272  ordiso2  6928  distrlem5prl  7418  distrlem5pru  7419  bndndx  9000  uzind2  9187  leexp1a  10379  cncongr1  11820  bj-inf2vnlem2  13340