Theorem 3com23 1147

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 1140	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 77	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1135	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  3coml  1148  syld3an2  1219  3anidm13  1230  eqreu  2798  f1ofveu  5601  acexmid  5612  dfsmo2  6006  f1oeng  6426  ltexprlemdisj  7109  ltexprlemfu  7114  recexprlemss1u  7139  mul32  7556  add32  7585  cnegexlem2  7602  subsub23  7631  subadd23  7638  addsub12  7639  subsub  7656  subsub3  7658  sub32  7660  suble  7862  lesub  7863  ltsub23  7864  ltsub13  7865  ltleadd  7868  div32ap  8098  div13ap  8099  div12ap  8100  divdiv32ap  8126  cju  8356  icc0r  9276  fzen  9389  elfz1b  9434  ioo0  9599  ico0  9601  ioc0  9602  expival  9856  expgt0  9887  expge0  9890  expge1  9891  shftval2  10157  abs3dif  10434  divalgb  10807