df-and Show Code edit
## Definition of AND
##
## Define conjunction, logical AND.
## This theorem writes the definition of AND without using the biconditional. The
## theorem df-an rewrites this definition in a more familiar
## form.
##
defthm (df-and wff (/\ ph ps) () ()
(-. (-> (-> (/\ ph ps) (-. (-> ph (-. ps))))
(-. (-> (-. (-> ph (-. ps))) (/\ ph ps)))))
(-. (-> ph (-. ps))) id
(-> (-. (-> ph (-. ps))) (-. (-> ph (-. ps))))
(-. (-> ph (-. ps))) id
(-> (-. (-> ph (-. ps))) (-. (-> ph (-. ps))))
preandi)
(-. (-> (-> (-. (-> ph (-. ps))) (-. (-> ph (-. ps)))) (-. (-> (-. (-> ph (-. ps))) (-. (-> ph (-. ps)))))))
edit