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  5411  f1o2ndf1  6464  brecop  6899  fiintim  7238  elpq  10049  xnn0lenn0nn0  10267  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  fzo1fzo0n0  10595  elfzodifsumelfzo  10619  ssfzo12  10642  ssfzo12bi  10643  facwordi  11178  fihashf1rn  11227  swrdswrdlem  11476  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  pfxccatin12lem2  11503  swrdccat  11507  reuccatpfxs1lem  11518  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  dfgcd2  12791  sqrt2irr  12940  lmodfopnelem1  14661  mpomulcn  15667  zabsle1  16118  gausslemma2dlem1a  16177  2lgsoddprm  16232  upgredg2vtx  16389  usgruspgrben  16427  usgredg2vlem2  16464  edg0usgr  16488  uspgr2wlkeq  16606  clwwlkn1loopb  16661  clwwlkext2edg  16663  clwwlknonex2lem2  16679  bj-inf2vnlem2  16997