Theorem com23 32

Description: Commutation of antecedents. Swap 2nd and 3rd.

Hypothesis

Ref	Expression
com3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
com23	|- (ph -> (ch -> (ps -> th)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		pm2.04 31	. 2 |- ((ps -> (ch -> th)) -> (ch -> (ps -> th)))
3	1, 2	syl 12	1 |- (ph -> (ch -> (ps -> th)))

Syntax hints:   -> wi 2

This theorem is referenced by:  com13 33  com3l 34  com24 37  a1dd 42  mpii 45  pm2.43a 60  pm2.86 63  impt 122  prth 429  elimant 505  pclem6 555  dedlem0b 568  dedlemb 570  3com23 616  meredith 644  eqs2 829  cbv1 845  sbequi 876  sbied 903  ralcom2 1314  reupick 1578  pwssun 1917  ssiun 2018  wefrc 2195  ordelord 2221  tz7.7 2224  onfr 2237  ordtr2 2257  onmindif 2312  limsuc 2361  limsssuc 2362  unizlim 2364  limomss 2378  findsg 2398  tfinds 2401  tfindsg 2402  funssres 2698  funcnvuni 2706  fv3 2839  funfvima2 2905  isoini 2938  f1oweOLD 2944  tfrlem1 2949  tz7.49 2997  abianfp 3000  omordi 3164  nnmord 3189  nnmcan 3190  nnaordex 3191  nnawordex 3192  omsmolem 3195  eceqopreq 3249  th3qlem1 3250  en3d 3304  xpdom2 3345  sdomen2 3380  mapenlem1 3384  mapenlem2 3385  pssnn 3428  suc11reg 3456  inf3lem2 3465  inf3lem5 3468  trcl 3489  zfregs 3491  aceq5lem5 3562  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodom 3613  unxpdomlem 3649  alephordi 3679  ltbtwnpq 3878  genpcd 3903  psslinpr 3929  prlem934 3933  ltaddpr 3934  ltexprlem3 3938  ltexprlem6 3941  ltexprlem7 3942  ltapr 3945  prlem936b 3948  prlem936 3949  suplem1pr 3955  suppsr2 4017  suppsr3 4018  negeu 4124  receu 4215  ltletrt 4290  nnsub 4450  nndiv 4453  sup2 4510  elnnz 4572  uzind 4603  uzwo 4605  uzwo2 4606  nnwoOLD 4608  zbtwnre 4619  qbtwnre 4650  xpnnen 4927  znnenlem 4929  infxpidmlem11 4943  chsscm 5147  ocin 5177  occl 5188  projlem26 5218  spansneleq 5475  spansnsst 5476  elspansn4t 5478  h1datom 5483  osumlem6 5535  spansncv 5542  cvnbtwnt 5718  spansncv2t 5725  mdi 5727  dmdbr 5731  dmdi 5732  cvexchlem 5759  atcv1 5768  atcvatlem 5770  atcvat2 5772  atcvat4 5775  mdsymlem3 5778  mdsymlem4 5779  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org