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  6562  f1oeng  7047  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  10345  fzen  10464  elfz1b  10514  ioo0  10711  ico0  10713  ioc0  10714  expgt0  11030  expge0  11033  expge1  11034  shftval2  11613  abs3dif  11894  divalgb  12717  nnwodc  12838  ctinf  13379  grpinvcnv  13932  mulgaddcom  14008  mulgneg2  14018  srgrmhm  14405  ringcom  14443  mulgass2  14470  opprrng  14491  opprring  14493  unitmulcl  14529  islmodd  14738  lmodcom  14779  rmodislmod  14797  restin  15402  cnpnei  15445  cnptoprest  15465  psmetsym  15555  xmetsym  15594