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  567  an31s  570  3imp31  1220  3imp21  1222  funopg  5358  f1o2ndf1  6388  brecop  6789  fiintim  7116  elpq  9873  xnn0lenn0nn0  10090  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  fzo1fzo0n0  10412  elfzodifsumelfzo  10436  ssfzo12  10459  ssfzo12bi  10460  facwordi  10992  fihashf1rn  11040  swrdswrdlem  11275  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  pfxccatin12lem2  11302  swrdccat  11306  reuccatpfxs1lem  11317  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  dfgcd2  12575  sqrt2irr  12724  lmodfopnelem1  14328  mpomulcn  15280  zabsle1  15718  gausslemma2dlem1a  15777  2lgsoddprm  15832  upgredg2vtx  15987  usgruspgrben  16025  usgredg2vlem2  16062  edg0usgr  16086  uspgr2wlkeq  16162  clwwlkn1loopb  16215  clwwlkext2edg  16217  clwwlknonex2lem2  16233  bj-inf2vnlem2  16502