List of theorems

List of theorems in peano_new/arithmetic/common/ifn.gh:

Ternary conditional for naturals

df-ifn-just Ternary expressions for naturals: (ph ? A : B)
(= (iota ({|} x (\/ (/\ ph (= x A)) (/\ (-. ph) (= x B))))) (iota ({|} y (\/ (/\ ph (= y A)) (/\ (-. ph) (= y B))))))
(= (ifn ph A B) (iota ({|} x (\/ (/\ ph (= x A)) (/\ (-. ph) (= x B))))))
ifn1 # <title> First branch of ternary expression </title>
(-> ph (= (ifn ph A B) A))
ifn2 # <title> Second branch of ternary expression </title>
(-> (-. ph) (= (ifn ph A B) B))
ifnbi1 # <title> Equivalence of predicate in ifn </title>
(-> (<-> ph ps) (= (ifn ph A B) (ifn ps A B)))
(<-> ph ps)(= (ifn ph A B) (ifn ps A B))
(-> ch (<-> ph ps))(-> ch (= (ifn ph A B) (ifn ps A B)))
ifneq2 # <title> Equality of first term for ifn </title>
(-> (= A B) (= (ifn ph A C) (ifn ph B C)))
(= A B)(= (ifn ph A C) (ifn ph B C))
(-> ps (= A B))(-> ps (= (ifn ph A C) (ifn ph B C)))
ifneq3 # <title> Equality of second term for ifn </title>
(-> (= A B) (= (ifn ph C A) (ifn ph C B)))
(= A B)(= (ifn ph C A) (ifn ph C B))
(-> ps (= A B))(-> ps (= (ifn ph C A) (ifn ph C B)))
BiReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (<-> ps ch)(-> ph (/\ ch th))
(-> (/\ (<-> ph ps) (= A B)) (= (ifn ph C A) (ifn ps C B)))
ifnbi123 # <title> Equivalence for ifn </title>
(-> (/\ (<-> ph ps) (/\ (= A C) (= B D))) (= (ifn ph A B) (ifn ps C D)))
(-> ph (<-> ps ch)) , (-> ph (= A B)) , (-> ph (= C D))(-> ph (= (ifn ps A C) (ifn ch B D)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)