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  6076  acexmid  6087  dfsmo2  6563  f1oeng  7049  ctssdc  7459  ltexprlemdisj  7979  ltexprlemfu  7984  recexprlemss1u  8009  mul32  8463  add32  8492  cnegexlem2  8509  subsub23  8538  subadd23  8545  addsub12  8546  subsub  8563  subsub3  8565  sub32  8567  suble  8775  lesub  8776  ltsub23  8777  ltsub13  8778  ltleadd  8781  div32ap  9030  div13ap  9031  div12ap  9032  divdiv32ap  9058  cju  9299  icc0r  10344  fzen  10463  elfz1b  10513  ioo0  10710  ico0  10712  ioc0  10713  expgt0  11029  expge0  11032  expge1  11033  shftval2  11612  abs3dif  11893  divalgb  12716  nnwodc  12837  ctinf  13378  grpinvcnv  13931  mulgaddcom  14007  mulgneg2  14017  srgrmhm  14404  ringcom  14442  mulgass2  14469  opprrng  14490  opprring  14492  unitmulcl  14528  islmodd  14737  lmodcom  14778  rmodislmod  14796  restin  15419  cnpnei  15462  cnptoprest  15482  psmetsym  15572  xmetsym  15611