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  5911  acexmid  5922  dfsmo2  6346  f1oeng  6817  ctssdc  7180  ltexprlemdisj  7675  ltexprlemfu  7680  recexprlemss1u  7705  mul32  8158  add32  8187  cnegexlem2  8204  subsub23  8233  subadd23  8240  addsub12  8241  subsub  8258  subsub3  8260  sub32  8262  suble  8469  lesub  8470  ltsub23  8471  ltsub13  8472  ltleadd  8475  div32ap  8721  div13ap  8722  div12ap  8723  divdiv32ap  8749  cju  8990  icc0r  10003  fzen  10120  elfz1b  10167  ioo0  10351  ico0  10353  ioc0  10354  expgt0  10666  expge0  10669  expge1  10670  shftval2  10993  abs3dif  11272  divalgb  12092  nnwodc  12213  ctinf  12657  grpinvcnv  13210  mulgaddcom  13286  mulgneg2  13296  srgrmhm  13560  ringcom  13597  mulgass2  13624  opprrng  13643  opprring  13645  unitmulcl  13679  islmodd  13859  lmodcom  13899  rmodislmod  13917  restin  14422  cnpnei  14465  cnptoprest  14485  psmetsym  14575  xmetsym  14614