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  8456  add32  8485  cnegexlem2  8502  subsub23  8531  subadd23  8538  addsub12  8539  subsub  8556  subsub3  8558  sub32  8560  suble  8768  lesub  8769  ltsub23  8770  ltsub13  8771  ltleadd  8774  div32ap  9022  div13ap  9023  div12ap  9024  divdiv32ap  9050  cju  9291  icc0r  10328  fzen  10447  elfz1b  10497  ioo0  10694  ico0  10696  ioc0  10697  expgt0  11009  expge0  11012  expge1  11013  shftval2  11591  abs3dif  11871  divalgb  12692  nnwodc  12813  ctinf  13321  grpinvcnv  13873  mulgaddcom  13949  mulgneg2  13959  srgrmhm  14298  ringcom  14336  mulgass2  14363  opprrng  14382  opprring  14384  unitmulcl  14420  islmodd  14629  lmodcom  14670  rmodislmod  14688  restin  15277  cnpnei  15320  cnptoprest  15340  psmetsym  15430  xmetsym  15469