Theorem 3com23 1212

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

Syntax hints:   -> wi 4   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3coml  1213  syld3an2  1297  3anidm13  1309  eqreu  2965  f1ofveu  5932  acexmid  5943  dfsmo2  6373  f1oeng  6848  ctssdc  7215  ltexprlemdisj  7719  ltexprlemfu  7724  recexprlemss1u  7749  mul32  8202  add32  8231  cnegexlem2  8248  subsub23  8277  subadd23  8284  addsub12  8285  subsub  8302  subsub3  8304  sub32  8306  suble  8513  lesub  8514  ltsub23  8515  ltsub13  8516  ltleadd  8519  div32ap  8765  div13ap  8766  div12ap  8767  divdiv32ap  8793  cju  9034  icc0r  10048  fzen  10165  elfz1b  10212  ioo0  10402  ico0  10404  ioc0  10405  expgt0  10717  expge0  10720  expge1  10721  shftval2  11137  abs3dif  11416  divalgb  12236  nnwodc  12357  ctinf  12801  grpinvcnv  13400  mulgaddcom  13482  mulgneg2  13492  srgrmhm  13756  ringcom  13793  mulgass2  13820  opprrng  13839  opprring  13841  unitmulcl  13875  islmodd  14055  lmodcom  14095  rmodislmod  14113  restin  14648  cnpnei  14691  cnptoprest  14711  psmetsym  14801  xmetsym  14840