Theorem 3com23 1209

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  3coml  1210  syld3an2  1285  3anidm13  1296  eqreu  2931  f1ofveu  5865  acexmid  5876  dfsmo2  6290  f1oeng  6759  ctssdc  7114  ltexprlemdisj  7607  ltexprlemfu  7612  recexprlemss1u  7637  mul32  8089  add32  8118  cnegexlem2  8135  subsub23  8164  subadd23  8171  addsub12  8172  subsub  8189  subsub3  8191  sub32  8193  suble  8399  lesub  8400  ltsub23  8401  ltsub13  8402  ltleadd  8405  div32ap  8651  div13ap  8652  div12ap  8653  divdiv32ap  8679  cju  8920  icc0r  9928  fzen  10045  elfz1b  10092  ioo0  10262  ico0  10264  ioc0  10265  expgt0  10555  expge0  10558  expge1  10559  shftval2  10837  abs3dif  11116  divalgb  11932  nnwodc  12039  ctinf  12433  grpinvcnv  12943  mulgaddcom  13012  mulgneg2  13022  srgrmhm  13182  ringcom  13219  mulgass2  13240  opprring  13254  unitmulcl  13287  islmodd  13388  lmodcom  13428  rmodislmod  13446  restin  13715  cnpnei  13758  cnptoprest  13778  psmetsym  13868  xmetsym  13907