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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  3coml  1241  syld3an2  1325  3anidm13  1337  eqreu  3018  f1ofveu  6063  acexmid  6074  dfsmo2  6548  f1oeng  7033  ctssdc  7443  ltexprlemdisj  7963  ltexprlemfu  7968  recexprlemss1u  7993  mul32  8446  add32  8475  cnegexlem2  8492  subsub23  8521  subadd23  8528  addsub12  8529  subsub  8546  subsub3  8548  sub32  8550  suble  8758  lesub  8759  ltsub23  8760  ltsub13  8761  ltleadd  8764  div32ap  9012  div13ap  9013  div12ap  9014  divdiv32ap  9040  cju  9281  icc0r  10307  fzen  10426  elfz1b  10475  ioo0  10672  ico0  10674  ioc0  10675  expgt0  10987  expge0  10990  expge1  10991  shftval2  11569  abs3dif  11849  divalgb  12670  nnwodc  12791  ctinf  13299  grpinvcnv  13850  mulgaddcom  13926  mulgneg2  13936  srgrmhm  14272  ringcom  14309  mulgass2  14336  opprrng  14355  opprring  14357  unitmulcl  14393  islmodd  14602  lmodcom  14642  rmodislmod  14660  restin  15200  cnpnei  15243  cnptoprest  15263  psmetsym  15353  xmetsym  15392