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  1221  expdcom  1485  nebidc  2480  sbcimdv  3095  prel12  3852  reusv3  4555  relcoi1  5266  oprabid  6045  poxp  6392  reldmtpos  6414  tfrlem9  6480  tfri3  6528  ordiso2  7225  distrlem5prl  7796  distrlem5pru  7797  bndndx  9391  uzind2  9582  leexp1a  10846  swrdswrdlem  11275  swrdswrd  11276  swrdccat3blem  11310  reuccatpfxs1lem  11317  cncongr1  12665  infpnlem1  12922  gausslemma2dlem1a  15777  uhgr2edg  16045  bj-inf2vnlem2  16502