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  2972  f1ofveu  5955  acexmid  5966  dfsmo2  6396  f1oeng  6871  ctssdc  7241  ltexprlemdisj  7754  ltexprlemfu  7759  recexprlemss1u  7784  mul32  8237  add32  8266  cnegexlem2  8283  subsub23  8312  subadd23  8319  addsub12  8320  subsub  8337  subsub3  8339  sub32  8341  suble  8548  lesub  8549  ltsub23  8550  ltsub13  8551  ltleadd  8554  div32ap  8800  div13ap  8801  div12ap  8802  divdiv32ap  8828  cju  9069  icc0r  10083  fzen  10200  elfz1b  10247  ioo0  10439  ico0  10441  ioc0  10442  expgt0  10754  expge0  10757  expge1  10758  shftval2  11252  abs3dif  11531  divalgb  12351  nnwodc  12472  ctinf  12916  grpinvcnv  13515  mulgaddcom  13597  mulgneg2  13607  srgrmhm  13871  ringcom  13908  mulgass2  13935  opprrng  13954  opprring  13956  unitmulcl  13990  islmodd  14170  lmodcom  14210  rmodislmod  14228  restin  14763  cnpnei  14806  cnptoprest  14826  psmetsym  14916  xmetsym  14955