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  2944  f1ofveu  5883  acexmid  5894  dfsmo2  6311  f1oeng  6782  ctssdc  7141  ltexprlemdisj  7634  ltexprlemfu  7639  recexprlemss1u  7664  mul32  8116  add32  8145  cnegexlem2  8162  subsub23  8191  subadd23  8198  addsub12  8199  subsub  8216  subsub3  8218  sub32  8220  suble  8426  lesub  8427  ltsub23  8428  ltsub13  8429  ltleadd  8432  div32ap  8678  div13ap  8679  div12ap  8680  divdiv32ap  8706  cju  8947  icc0r  9955  fzen  10072  elfz1b  10119  ioo0  10289  ico0  10291  ioc0  10292  expgt0  10583  expge0  10586  expge1  10587  shftval2  10866  abs3dif  11145  divalgb  11961  nnwodc  12068  ctinf  12480  grpinvcnv  13009  mulgaddcom  13083  mulgneg2  13093  srgrmhm  13345  ringcom  13382  mulgass2  13407  opprrng  13424  opprring  13426  unitmulcl  13460  islmodd  13606  lmodcom  13646  rmodislmod  13664  restin  14128  cnpnei  14171  cnptoprest  14191  psmetsym  14281  xmetsym  14320