Theorem 3com23 1145

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

Syntax hints:   -> wi 4   /\ w3a 920

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 922

This theorem is referenced by:  3coml  1146  syld3an2  1217  3anidm13  1228  eqreu  2785  f1ofveu  5531  acexmid  5542  dfsmo2  5936  f1oeng  6304  ltexprlemdisj  6858  ltexprlemfu  6863  recexprlemss1u  6888  mul32  7305  add32  7334  cnegexlem2  7351  subsub23  7380  subadd23  7387  addsub12  7388  subsub  7405  subsub3  7407  sub32  7409  suble  7611  lesub  7612  ltsub23  7613  ltsub13  7614  ltleadd  7617  div32ap  7847  div13ap  7848  div12ap  7849  divdiv32ap  7875  cju  8105  icc0r  9025  fzen  9138  elfz1b  9183  ioo0  9346  ico0  9348  ioc0  9349  expival  9575  expgt0  9606  expge0  9609  expge1  9610  shftval2  9852  abs3dif  10129  divalgb  10469