DeZero.iff_mp

Énoncé

∀ {a : Prop} {b : Prop} (h : a ↔ b) (ha : a), b

D’une équivalence et de son membre gauche, tire le membre droit.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Sens direct d'une équivalence. -/
theorem iff_mp {a b : Prop} (h : a ↔ b) (ha : a) : b :=
  Iff.rec (motive := fun _ => b) (fun hab _ => hab ha) h