Theorem 3com23 1235

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  3coml  1236  syld3an2  1320  3anidm13  1332  eqreu  2998  f1ofveu  6006  acexmid  6017  dfsmo2  6453  f1oeng  6930  ctssdc  7312  ltexprlemdisj  7826  ltexprlemfu  7831  recexprlemss1u  7856  mul32  8309  add32  8338  cnegexlem2  8355  subsub23  8384  subadd23  8391  addsub12  8392  subsub  8409  subsub3  8411  sub32  8413  suble  8620  lesub  8621  ltsub23  8622  ltsub13  8623  ltleadd  8626  div32ap  8872  div13ap  8873  div12ap  8874  divdiv32ap  8900  cju  9141  icc0r  10161  fzen  10278  elfz1b  10325  ioo0  10520  ico0  10522  ioc0  10523  expgt0  10835  expge0  10838  expge1  10839  shftval2  11404  abs3dif  11683  divalgb  12504  nnwodc  12625  ctinf  13069  grpinvcnv  13669  mulgaddcom  13751  mulgneg2  13761  srgrmhm  14026  ringcom  14063  mulgass2  14090  opprrng  14109  opprring  14111  unitmulcl  14146  islmodd  14326  lmodcom  14366  rmodislmod  14384  restin  14919  cnpnei  14962  cnptoprest  14982  psmetsym  15072  xmetsym  15111