Theorem com13 80

Description: Commutation of antecedents. Swap 1st and 3rd. (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
com13	|- ( ch -> ( ps -> ( ph -> th ) ) )

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com3r 79	. 2 |- ( ch -> ( ph -> ( ps -> th ) ) )
3	2	com23 78	1 |- ( ch -> ( ps -> ( 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:  com24  87  an13s  569  an31s  572  3imp31  1222  3imp21  1224  funopg  5359  f1o2ndf1  6395  brecop  6796  fiintim  7125  elpq  9885  xnn0lenn0nn0  10102  elfz0ubfz0  10362  elfz0fzfz0  10363  fz0fzelfz0  10364  fz0fzdiffz0  10367  fzo1fzo0n0  10425  elfzodifsumelfzo  10449  ssfzo12  10472  ssfzo12bi  10473  facwordi  11005  fihashf1rn  11053  swrdswrdlem  11291  swrdswrd  11292  wrd2ind  11310  swrdccatin1  11312  pfxccatin12lem2  11318  swrdccat  11322  reuccatpfxs1lem  11333  oddnn02np1  12461  oddge22np1  12462  evennn02n  12463  evennn2n  12464  dfgcd2  12605  sqrt2irr  12754  lmodfopnelem1  14359  mpomulcn  15316  zabsle1  15754  gausslemma2dlem1a  15813  2lgsoddprm  15868  upgredg2vtx  16025  usgruspgrben  16063  usgredg2vlem2  16100  edg0usgr  16124  uspgr2wlkeq  16242  clwwlkn1loopb  16297  clwwlkext2edg  16299  clwwlknonex2lem2  16315  bj-inf2vnlem2  16624