Theorem 3com23 1187

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3com23	|- ( ( ph /\ ch /\ ps ) -> th )

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1180	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1175	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3coml  1188  syld3an2  1263  3anidm13  1274  eqreu  2871  f1ofveu  5755  acexmid  5766  dfsmo2  6177  f1oeng  6644  ctssdc  6991  ltexprlemdisj  7407  ltexprlemfu  7412  recexprlemss1u  7437  mul32  7885  add32  7914  cnegexlem2  7931  subsub23  7960  subadd23  7967  addsub12  7968  subsub  7985  subsub3  7987  sub32  7989  suble  8195  lesub  8196  ltsub23  8197  ltsub13  8198  ltleadd  8201  div32ap  8445  div13ap  8446  div12ap  8447  divdiv32ap  8473  cju  8712  icc0r  9702  fzen  9816  elfz1b  9863  ioo0  10030  ico0  10032  ioc0  10033  expgt0  10319  expge0  10322  expge1  10323  shftval2  10591  abs3dif  10870  divalgb  11611  ctinf  11932  restin  12334  cnpnei  12377  cnptoprest  12397  psmetsym  12487  xmetsym  12526