Theorem com13 33

Description: Commutation of antecedents. Swap 1st and 3rd.

Hypothesis

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

Assertion

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

Proof of Theorem com13

Step	Hyp	Ref	Expression
1		com3.1	. . . 4 |- (ph -> (ps -> (ch -> th)))
2	1	com12 11	. . 3 |- (ps -> (ph -> (ch -> th)))
3	2	com23 32	. 2 |- (ps -> (ch -> (ph -> th)))
4	3	com12 11	1 |- (ch -> (ps -> (ph -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  com3l 34  com14 38  ancom13s 488  ancom31s 491  ordsssuc2 3059  peano5 3153  funopg 3547  isomin 3899  abianfp 3962  omordi 4197  brecop 4306  isfinite2OLD 4546  fiint 4559  fiintOLD 4560  aceq5 4740  aceq6b 4742  carduni 4858  mulgt0sr 5214  squeeze0 5924  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  supxrunb2 6090  zmax 6220  facwordit 6944  infxpidmlem7 7558  infxpidmlem12 7563  cnpco 7769  iscncl 7770  cncnplem4 7777  opnin 7869  lmle 7960  bcthlem1 7999  bcthlem28 8026  bcthlem33 8031  spwmo 8656  projlem15 9200  projlem26 9211  shmods 9362  kbass6t 10054  mdsymlem6 10335  mdsymlem7 10336  cdj3lem2a 10363  cdj3lem3a 10366  uninqs 10441  fiiu 10453  fiiuOLD 10454  11st22nd 10458  cdrci 10494  sfseqeq 10543  unpde2eg2 10544  set2elt 10545  top2usne 10549  homindlem3 10551  fipfil2 10564  fipfil2OLD 10565  efilcp 10572  efilcpOLD 10573  filint2 10574  filint2OLD 10575  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588  rcfpfillem6 10595  rcfpfillem6OLD 10596  iintlem1 10632  cmpassoh 10729  ismonc 10742  cmpmon 10743  icmpmon 10744

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain