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  5367  f1o2ndf1  6402  brecop  6837  fiintim  7166  elpq  9944  xnn0lenn0nn0  10161  elfz0ubfz0  10422  elfz0fzfz0  10423  fz0fzelfz0  10424  fz0fzdiffz0  10427  fzo1fzo0n0  10485  elfzodifsumelfzo  10509  ssfzo12  10532  ssfzo12bi  10533  facwordi  11065  fihashf1rn  11113  swrdswrdlem  11351  swrdswrd  11352  wrd2ind  11370  swrdccatin1  11372  pfxccatin12lem2  11378  swrdccat  11382  reuccatpfxs1lem  11393  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  dfgcd2  12665  sqrt2irr  12814  lmodfopnelem1  14420  mpomulcn  15377  zabsle1  15818  gausslemma2dlem1a  15877  2lgsoddprm  15932  upgredg2vtx  16089  usgruspgrben  16127  usgredg2vlem2  16164  edg0usgr  16188  uspgr2wlkeq  16306  clwwlkn1loopb  16361  clwwlkext2edg  16363  clwwlknonex2lem2  16379  bj-inf2vnlem2  16687