Proof that '(p -> q -> z) <-> ((p /\ q) -> z)'.

impl.v

Section ImplicationProof.

  Variables p q z : Prop.

  Lemma T1: (p -> q -> z) ->  ((p /\ q) -> z).
    intros L P.
    elim P.
    trivial.
  Save.

  Lemma T2: ((p /\ q) -> z) -> (p -> q -> z).
    intros.
    cut (p /\ q); [trivial | split; [trivial | trivial]].
  Save.

  Lemma ImplicationChain: (p -> q -> z) <->  ((p /\ q) -> z).
    split; [apply T1 | apply T2].
  Qed.

End ImplicationProof.