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  2965  f1ofveu  5934  acexmid  5945  dfsmo2  6375  f1oeng  6850  ctssdc  7217  ltexprlemdisj  7721  ltexprlemfu  7726  recexprlemss1u  7751  mul32  8204  add32  8233  cnegexlem2  8250  subsub23  8279  subadd23  8286  addsub12  8287  subsub  8304  subsub3  8306  sub32  8308  suble  8515  lesub  8516  ltsub23  8517  ltsub13  8518  ltleadd  8521  div32ap  8767  div13ap  8768  div12ap  8769  divdiv32ap  8795  cju  9036  icc0r  10050  fzen  10167  elfz1b  10214  ioo0  10404  ico0  10406  ioc0  10407  expgt0  10719  expge0  10722  expge1  10723  shftval2  11170  abs3dif  11449  divalgb  12269  nnwodc  12390  ctinf  12834  grpinvcnv  13433  mulgaddcom  13515  mulgneg2  13525  srgrmhm  13789  ringcom  13826  mulgass2  13853  opprrng  13872  opprring  13874  unitmulcl  13908  islmodd  14088  lmodcom  14128  rmodislmod  14146  restin  14681  cnpnei  14724  cnptoprest  14744  psmetsym  14834  xmetsym  14873