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  1223  3imp21  1225  funopg  5386  f1o2ndf1  6424  brecop  6859  fiintim  7191  elpq  9981  xnn0lenn0nn0  10198  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  fzo1fzo0n0  10522  elfzodifsumelfzo  10546  ssfzo12  10569  ssfzo12bi  10570  facwordi  11102  fihashf1rn  11151  swrdswrdlem  11396  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  pfxccatin12lem2  11423  swrdccat  11427  reuccatpfxs1lem  11438  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  dfgcd2  12710  sqrt2irr  12859  lmodfopnelem1  14472  mpomulcn  15431  zabsle1  15872  gausslemma2dlem1a  15931  2lgsoddprm  15986  upgredg2vtx  16143  usgruspgrben  16181  usgredg2vlem2  16218  edg0usgr  16242  uspgr2wlkeq  16360  clwwlkn1loopb  16415  clwwlkext2edg  16417  clwwlknonex2lem2  16433  bj-inf2vnlem2  16741