Theorem 3com23 1236

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  3coml  1237  syld3an2  1321  3anidm13  1333  eqreu  2999  f1ofveu  6016  acexmid  6027  dfsmo2  6496  f1oeng  6973  ctssdc  7372  ltexprlemdisj  7886  ltexprlemfu  7891  recexprlemss1u  7916  mul32  8368  add32  8397  cnegexlem2  8414  subsub23  8443  subadd23  8450  addsub12  8451  subsub  8468  subsub3  8470  sub32  8472  suble  8679  lesub  8680  ltsub23  8681  ltsub13  8682  ltleadd  8685  div32ap  8931  div13ap  8932  div12ap  8933  divdiv32ap  8959  cju  9200  icc0r  10222  fzen  10340  elfz1b  10387  ioo0  10582  ico0  10584  ioc0  10585  expgt0  10897  expge0  10900  expge1  10901  shftval2  11466  abs3dif  11745  divalgb  12566  nnwodc  12687  ctinf  13131  grpinvcnv  13731  mulgaddcom  13813  mulgneg2  13823  srgrmhm  14088  ringcom  14125  mulgass2  14152  opprrng  14171  opprring  14173  unitmulcl  14208  islmodd  14389  lmodcom  14429  rmodislmod  14447  restin  14987  cnpnei  15030  cnptoprest  15050  psmetsym  15140  xmetsym  15179