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  3094  prel12  3849  reusv3  4551  relcoi1  5260  oprabid  6039  poxp  6384  reldmtpos  6405  tfrlem9  6471  tfri3  6519  ordiso2  7213  distrlem5prl  7784  distrlem5pru  7785  bndndx  9379  uzind2  9570  leexp1a  10828  swrdswrdlem  11252  swrdswrd  11253  swrdccat3blem  11287  reuccatpfxs1lem  11294  cncongr1  12641  infpnlem1  12898  gausslemma2dlem1a  15753  uhgr2edg  16020  bj-inf2vnlem2  16417