Theorem 3com23 1199

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 1192	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1183	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  3coml  1200  syld3an2  1275  3anidm13  1286  eqreu  2918  f1ofveu  5830  acexmid  5841  dfsmo2  6255  f1oeng  6723  ctssdc  7078  ltexprlemdisj  7547  ltexprlemfu  7552  recexprlemss1u  7577  mul32  8028  add32  8057  cnegexlem2  8074  subsub23  8103  subadd23  8110  addsub12  8111  subsub  8128  subsub3  8130  sub32  8132  suble  8338  lesub  8339  ltsub23  8340  ltsub13  8341  ltleadd  8344  div32ap  8588  div13ap  8589  div12ap  8590  divdiv32ap  8616  cju  8856  icc0r  9862  fzen  9978  elfz1b  10025  ioo0  10195  ico0  10197  ioc0  10198  expgt0  10488  expge0  10491  expge1  10492  shftval2  10768  abs3dif  11047  divalgb  11862  nnwodc  11969  ctinf  12363  restin  12816  cnpnei  12859  cnptoprest  12879  psmetsym  12969  xmetsym  13008