Theorem 3com23 1240

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3coml  1241  syld3an2  1325  3anidm13  1337  eqreu  3018  f1ofveu  6073  acexmid  6084  dfsmo2  6558  f1oeng  7043  ctssdc  7454  ltexprlemdisj  7974  ltexprlemfu  7979  recexprlemss1u  8004  mul32  8458  add32  8487  cnegexlem2  8504  subsub23  8533  subadd23  8540  addsub12  8541  subsub  8558  subsub3  8560  sub32  8562  suble  8770  lesub  8771  ltsub23  8772  ltsub13  8773  ltleadd  8776  div32ap  9025  div13ap  9026  div12ap  9027  divdiv32ap  9053  cju  9294  icc0r  10339  fzen  10458  elfz1b  10508  ioo0  10705  ico0  10707  ioc0  10708  expgt0  11024  expge0  11027  expge1  11028  shftval2  11607  abs3dif  11888  divalgb  12711  nnwodc  12832  ctinf  13373  grpinvcnv  13926  mulgaddcom  14002  mulgneg2  14012  srgrmhm  14382  ringcom  14420  mulgass2  14447  opprrng  14466  opprring  14468  unitmulcl  14504  islmodd  14713  lmodcom  14754  rmodislmod  14772  restin  15368  cnpnei  15411  cnptoprest  15431  psmetsym  15521  xmetsym  15560