Theorem com3l 80

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 78	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com3r 78	1 |- ( ps -> ( ch -> ( ph -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com4l  83  impd  251  expdcom  1376  nebidc  2335  sbcimdv  2904  prel12  3615  reusv3  4282  relcoi1  4962  oprabid  5681  poxp  5997  reldmtpos  6018  tfrlem9  6084  tfri3  6132  ordiso2  6728  distrlem5prl  7145  distrlem5pru  7146  bndndx  8672  uzind2  8858  leexp1a  10010  cncongr1  11363  bj-inf2vnlem2  11866