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  5995  acexmid  6006  dfsmo2  6439  f1oeng  6916  ctssdc  7291  ltexprlemdisj  7804  ltexprlemfu  7809  recexprlemss1u  7834  mul32  8287  add32  8316  cnegexlem2  8333  subsub23  8362  subadd23  8369  addsub12  8370  subsub  8387  subsub3  8389  sub32  8391  suble  8598  lesub  8599  ltsub23  8600  ltsub13  8601  ltleadd  8604  div32ap  8850  div13ap  8851  div12ap  8852  divdiv32ap  8878  cju  9119  icc0r  10134  fzen  10251  elfz1b  10298  ioo0  10491  ico0  10493  ioc0  10494  expgt0  10806  expge0  10809  expge1  10810  shftval2  11353  abs3dif  11632  divalgb  12452  nnwodc  12573  ctinf  13017  grpinvcnv  13617  mulgaddcom  13699  mulgneg2  13709  srgrmhm  13973  ringcom  14010  mulgass2  14037  opprrng  14056  opprring  14058  unitmulcl  14093  islmodd  14273  lmodcom  14313  rmodislmod  14331  restin  14866  cnpnei  14909  cnptoprest  14929  psmetsym  15019  xmetsym  15058