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  11388  abs3dif  11667  divalgb  12488  nnwodc  12609  ctinf  13053  grpinvcnv  13653  mulgaddcom  13735  mulgneg2  13745  srgrmhm  14010  ringcom  14047  mulgass2  14074  opprrng  14093  opprring  14095  unitmulcl  14130  islmodd  14310  lmodcom  14350  rmodislmod  14368  restin  14903  cnpnei  14946  cnptoprest  14966  psmetsym  15056  xmetsym  15095