Logiweb codex of peano commutativity in pyk

Up Help

ref-2-id-55	axiom prime a one
ref-2-id-56	axiom prime a two
ref-2-id-57	axiom prime a three
ref-2-id-58	axiom prime a four
ref-2-id-59	axiom prime a five
ref-2-id-60	axiom prime s one
ref-2-id-61	axiom prime s two
ref-2-id-62	axiom prime s three
ref-2-id-63	axiom prime s four
ref-2-id-64	axiom prime s five
ref-2-id-65	axiom prime s six
ref-2-id-66	axiom prime s seven
ref-2-id-67	axiom prime s eight
ref-2-id-68	axiom prime s nine
ref-2-id-69	rule prime mp
ref-2-id-70	rule prime gen
ref-0-id-0	peano commutativity
ref-0-id-1	weakening
ref-0-id-2	conditioned mp prime
ref-0-id-3	permute antecedents
ref-0-id-4	imply transitivity
ref-0-id-5	equal reflexivity
ref-0-id-6	equal symmetry
ref-0-id-7	equal transitivity
ref-0-id-8	mendelson three two d
ref-0-id-9	substitution macro
ref-0-id-10	mendelson three two f base
ref-0-id-11	mendelson three two f induction
ref-0-id-12	mendelson three two f
ref-0-id-13	mendelson three two g base
ref-0-id-14	mendelson three two g induction
ref-0-id-15	mendelson three two g
ref-0-id-16	mendelson three two g rt switch
ref-0-id-17	add one
ref-0-id-18	mendelson three two d rule
ref-0-id-19	mendelson three two d conditioned rule
ref-0-id-20	equal transitivity rule
ref-0-id-21	equal transitivity conditioned rule
ref-0-id-22	plus commutativity base
ref-0-id-23	plus commutativity induction
ref-0-id-24	plus commutativity
ref-0-id-25	double mp prime
ref-0-id-26	induction macro
ref-0-id-27	equal symmetry rule
ref-0-id-28	double conditioned mp prime