Theorem: Usa2015P1.iff_comm (Compfiles/Usa2015P1.lean)

State before:
a b c : Prop
⊢ (a → c) → (b → c) → (c → (a ↔ b)) → (a ↔ b)
Tactic:
tauto
State after:
no goals