∀ A B return, A ⇒ B ⇒ return ⇒ A ∧ B ⇒ return

Axiom match_And_prop : forall (A:Prop), forall (B:Prop), forall (return_:Prop), (A -> B -> return_) -> (And A B) -> return_

axiom match_And_prop : \forall (A:Prop). \forall (B:Prop). \forall (return_:Prop). ((A) -> (B) -> return_) -> ((And) A B) -> return_

axiom match_And_prop : forall (A:Prop) , forall (B:Prop) , forall (return:Prop) , ((A) -> (B) -> return) -> ((((connectives.And) ) (A)) (B)) -> return

match_And_prop : AXIOM (FORALL(A:bool):(FORALL(B:bool):(FORALL(return:bool):((A => (B => return)) => (connectives_sttfa.sttfa_And(A)(B) => return)))))

Printing for OpenTheory is not working at the moment.