Description: A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | aibandbiaiffaiffb | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( 𝜑 ↔ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ) | |
2 | 1 | bicomi | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( 𝜑 ↔ 𝜓 ) ) |