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  1187  expdcom  1430  nebidc  2416  sbcimdv  3016  prel12  3751  reusv3  4438  relcoi1  5135  oprabid  5874  poxp  6200  reldmtpos  6221  tfrlem9  6287  tfri3  6335  ordiso2  7000  distrlem5prl  7527  distrlem5pru  7528  bndndx  9113  uzind2  9303  leexp1a  10510  cncongr1  12035  infpnlem1  12289  bj-inf2vnlem2  13853