Theorem Marketplace

Theorem Details

theorem imp_trans (P Q R : Prop) (h1 : P -> Q) (h2 : Q -> R) : P -> R := by sorry

Bounty: 0.0014 ETH

Status: Closed

Proof

theorem imp_trans (P Q R : Prop) (h1 : P -> Q) (h2 : Q -> R) : P -> R := by intro p; apply h2; apply h1; exact p

Back to Bounties