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  573  an31s  576  3imp31  1227  3imp21  1229  funopg  5406  f1o2ndf1  6454  brecop  6889  fiintim  7228  elpq  10028  xnn0lenn0nn0  10246  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  fzo1fzo0n0  10573  elfzodifsumelfzo  10597  ssfzo12  10620  ssfzo12bi  10621  facwordi  11156  fihashf1rn  11205  swrdswrdlem  11454  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  pfxccatin12lem2  11481  swrdccat  11485  reuccatpfxs1lem  11496  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  dfgcd2  12769  sqrt2irr  12918  lmodfopnelem1  14633  mpomulcn  15590  zabsle1  16032  gausslemma2dlem1a  16091  2lgsoddprm  16146  upgredg2vtx  16303  usgruspgrben  16341  usgredg2vlem2  16378  edg0usgr  16402  uspgr2wlkeq  16520  clwwlkn1loopb  16575  clwwlkext2edg  16577  clwwlknonex2lem2  16593  bj-inf2vnlem2  16911