Theorem 3com23 1211

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 1204	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1195	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1307  eqreu  2952  f1ofveu  5906  acexmid  5917  dfsmo2  6340  f1oeng  6811  ctssdc  7172  ltexprlemdisj  7666  ltexprlemfu  7671  recexprlemss1u  7696  mul32  8149  add32  8178  cnegexlem2  8195  subsub23  8224  subadd23  8231  addsub12  8232  subsub  8249  subsub3  8251  sub32  8253  suble  8459  lesub  8460  ltsub23  8461  ltsub13  8462  ltleadd  8465  div32ap  8711  div13ap  8712  div12ap  8713  divdiv32ap  8739  cju  8980  icc0r  9992  fzen  10109  elfz1b  10156  ioo0  10328  ico0  10330  ioc0  10331  expgt0  10643  expge0  10646  expge1  10647  shftval2  10970  abs3dif  11249  divalgb  12066  nnwodc  12173  ctinf  12587  grpinvcnv  13140  mulgaddcom  13216  mulgneg2  13226  srgrmhm  13490  ringcom  13527  mulgass2  13554  opprrng  13573  opprring  13575  unitmulcl  13609  islmodd  13789  lmodcom  13829  rmodislmod  13847  restin  14344  cnpnei  14387  cnptoprest  14407  psmetsym  14497  xmetsym  14536