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  1198  3imp21  1200  funopg  5292  f1o2ndf1  6286  brecop  6684  fiintim  6992  elpq  9723  xnn0lenn0nn0  9940  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  fzo1fzo0n0  10259  elfzodifsumelfzo  10277  ssfzo12  10300  ssfzo12bi  10301  facwordi  10832  fihashf1rn  10880  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  dfgcd2  12181  sqrt2irr  12330  lmodfopnelem1  13880  mpomulcn  14802  zabsle1  15240  gausslemma2dlem1a  15299  2lgsoddprm  15354  bj-inf2vnlem2  15617