Theorem 3com23 1233

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  3coml  1234  syld3an2  1318  3anidm13  1330  eqreu  2995  f1ofveu  5989  acexmid  6000  dfsmo2  6433  f1oeng  6908  ctssdc  7280  ltexprlemdisj  7793  ltexprlemfu  7798  recexprlemss1u  7823  mul32  8276  add32  8305  cnegexlem2  8322  subsub23  8351  subadd23  8358  addsub12  8359  subsub  8376  subsub3  8378  sub32  8380  suble  8587  lesub  8588  ltsub23  8589  ltsub13  8590  ltleadd  8593  div32ap  8839  div13ap  8840  div12ap  8841  divdiv32ap  8867  cju  9108  icc0r  10122  fzen  10239  elfz1b  10286  ioo0  10479  ico0  10481  ioc0  10482  expgt0  10794  expge0  10797  expge1  10798  shftval2  11337  abs3dif  11616  divalgb  12436  nnwodc  12557  ctinf  13001  grpinvcnv  13601  mulgaddcom  13683  mulgneg2  13693  srgrmhm  13957  ringcom  13994  mulgass2  14021  opprrng  14040  opprring  14042  unitmulcl  14077  islmodd  14257  lmodcom  14297  rmodislmod  14315  restin  14850  cnpnei  14893  cnptoprest  14913  psmetsym  15003  xmetsym  15042