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  2956  f1ofveu  5910  acexmid  5921  dfsmo2  6345  f1oeng  6816  ctssdc  7179  ltexprlemdisj  7673  ltexprlemfu  7678  recexprlemss1u  7703  mul32  8156  add32  8185  cnegexlem2  8202  subsub23  8231  subadd23  8238  addsub12  8239  subsub  8256  subsub3  8258  sub32  8260  suble  8467  lesub  8468  ltsub23  8469  ltsub13  8470  ltleadd  8473  div32ap  8719  div13ap  8720  div12ap  8721  divdiv32ap  8747  cju  8988  icc0r  10001  fzen  10118  elfz1b  10165  ioo0  10349  ico0  10351  ioc0  10352  expgt0  10664  expge0  10667  expge1  10668  shftval2  10991  abs3dif  11270  divalgb  12090  nnwodc  12203  ctinf  12647  grpinvcnv  13200  mulgaddcom  13276  mulgneg2  13286  srgrmhm  13550  ringcom  13587  mulgass2  13614  opprrng  13633  opprring  13635  unitmulcl  13669  islmodd  13849  lmodcom  13889  rmodislmod  13907  restin  14412  cnpnei  14455  cnptoprest  14475  psmetsym  14565  xmetsym  14604