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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  87  an13s  573  an31s  576  3imp31  1227  3imp21  1229  funopg  5414  f1o2ndf1  6468  brecop  6904  fiintim  7244  elpq  10065  xnn0lenn0nn0  10283  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  fzo1fzo0n0  10611  elfzodifsumelfzo  10635  ssfzo12  10658  ssfzo12bi  10659  facwordi  11199  fihashf1rn  11248  swrdswrdlem  11497  swrdswrd  11498  wrd2ind  11516  swrdccatin1  11518  pfxccatin12lem2  11524  swrdccat  11528  reuccatpfxs1lem  11539  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  dfgcd2  12815  sqrt2irr  12965  lmodfopnelem1  14769  mpomulcn  15809  zabsle1  16340  gausslemma2dlem1a  16399  2lgsoddprm  16454  upgredg2vtx  16611  usgruspgrben  16649  usgredg2vlem2  16686  edg0usgr  16710  uspgr2wlkeq  16828  clwwlkn1loopb  16883  clwwlkext2edg  16885  clwwlknonex2lem2  16901  bj-inf2vnlem2  17219