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  6073  acexmid  6084  dfsmo2  6558  f1oeng  7043  ctssdc  7453  ltexprlemdisj  7973  ltexprlemfu  7978  recexprlemss1u  8003  mul32  8457  add32  8486  cnegexlem2  8503  subsub23  8532  subadd23  8539  addsub12  8540  subsub  8557  subsub3  8559  sub32  8561  suble  8769  lesub  8770  ltsub23  8771  ltsub13  8772  ltleadd  8775  div32ap  9024  div13ap  9025  div12ap  9026  divdiv32ap  9052  cju  9293  icc0r  10338  fzen  10457  elfz1b  10507  ioo0  10704  ico0  10706  ioc0  10707  expgt0  11022  expge0  11025  expge1  11026  shftval2  11605  abs3dif  11886  divalgb  12708  nnwodc  12829  ctinf  13370  grpinvcnv  13922  mulgaddcom  13998  mulgneg2  14008  srgrmhm  14347  ringcom  14385  mulgass2  14412  opprrng  14431  opprring  14433  unitmulcl  14469  islmodd  14678  lmodcom  14719  rmodislmod  14737  restin  15326  cnpnei  15369  cnptoprest  15389  psmetsym  15479  xmetsym  15518