∀ A B, A ∧ B ⇒ B

Theorem proj2 : forall (A:Prop), forall (B:Prop), (connectives.And A B) -> B.

theorem proj2 : \forall (A:Prop). \forall (B:Prop). ((And) A B) -> B.

theorem proj2 : forall (A:Prop) , forall (B:Prop) , ((((connectives.And) ) (A)) (B)) -> B.

proj2 : LEMMA (FORALL(A:bool):(FORALL(B:bool):(connectives_sttfa_th.sttfa_And(A)(B) => B)))

Printing for OpenTheory is not working at the moment.