df-an Show Code edit
## Definition of AND
## Define conjunction, logical AND.
## This theorem is based on an earlier definition of AND which
## did not use the biconditional. This theorem writes the definition of AND in a more
## familiar form using the biconditional.
##
thm (df-an () () (<-> (/\ ph ps) (-. (-> ph (-. ps))))
ph ps df-and-1
(-> (/\ ph ps) (-. (-> ph (-. ps))))
ph ps df-and-2
(-> (-. (-> ph (-. ps))) (/\ ph ps))
impbii
(<-> (/\ ph ps) (-. (-> ph (-. ps))))
)
edit