connectives.or_intror
∀ A B, B ⇒ A ∨ B
Axiom or_intror : forall (A:Prop), forall (B:Prop), B -> Or A B
axiom or_intror : \forall (A:Prop). \forall (B:Prop). (B) -> (Or) A B
axiom or_intror : forall (A:Prop) , forall (B:Prop) , (B) -> (((connectives.Or) ) (A)) (B)
or_intror : AXIOM (FORALL(A:bool):(FORALL(B:bool):(B => connectives_sttfa.sttfa_Or(A)(B))))
Printing for OpenTheory is not working at the moment.