variables p q : Prop theorem and_swap : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from and.intro (and.right h) (and.left h)) (assume h : q ∧ p, show p ∧ q, from and.intro (and.right h) (and.left h)) variable h : q ∧ p -- 1ª demostración example : p ∧ q := iff.mpr (and_swap p q) h -- 2ª demostración example : p ∧ q := (and_swap p q).mpr h