Chain implications

1/4 ~12 minlean

Compose two logical implications.

2 lines · Lean 4

theorem chain (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
  sorry

Objectifs

Indices

Voir la solution

theorem chain (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
  intro hPQ hQR hP
  exact hQR (hPQ hP)