		Search-engine friendly clone of the ACL2 documentation.

And4

Function: and4

(defun and4 (a b c d)
  (declare (xargs :guard t))
  (let ((__function__ 'and4))
    (declare (ignorable __function__))
    (and a b c d)))

Theorem: and4-forward

(defthm and4-forward
  (implies (and4 a b c d) (and a b c d))
  :rule-classes :forward-chaining)