gistfile1.txt

Section ZadanieOne.

Variables A B C D : Prop. 

Theorem impl_rozdz : (A -> B) -> (A -> C) -> A -> B -> C.
Proof.
Qed.

Theorem impl_komp : (A -> B) -> (B -> C) -> A -> C.
Proof.
Qed.

Theorem impl_perm : (A -> B -> C) -> B -> A -> C. 
Proof.
Qed.

Theorem impl_conj : A -> B -> A /\ B. 
Proof.
Qed.

Theorem conj_elim_l : A /\ B -> A. 
Proof.
Qed.

Theorem disj_intro_l : A -> A \/ B.
Proof.
Qed.

Theorem rozl_elim : A \/ B -> (A -> C) -> (B -> C) -> C. 
Proof.
Qed.

Theorem diamencik : (A -> B) -> (A -> C) -> (B -> C -> D) -> A -> D.
Proof.
Qed.

Theorem slaby_peirce : ((((A -> B) -> A) -> A) -> B) -> B.
Proof.
Qed.

Theorem rozl_impl_rozdz : (A \/ B -> C) -> (A -> C) /\ (B -> C).
Proof.
Qed.
 
Theorem rozl_impl_rozdz_odw : (A -> C) /\ (B -> C) -> A \/ B -> C.
Proof.
Qed.

Theorem curry : (A /\ B -> C) -> A -> B -> C.
Proof.
Qed.

Theorem uncurry : (A -> B -> C) -> A /\ B -> C.
Proof.
Qed.

End ZadanieOne.