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  1197  expdcom  1442  nebidc  2427  sbcimdv  3030  prel12  3773  reusv3  4462  relcoi1  5162  oprabid  5909  poxp  6235  reldmtpos  6256  tfrlem9  6322  tfri3  6370  ordiso2  7036  distrlem5prl  7587  distrlem5pru  7588  bndndx  9177  uzind2  9367  leexp1a  10577  cncongr1  12105  infpnlem1  12359  bj-inf2vnlem2  14808