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 | |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( ph <-> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi2 | |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) |
|
2 | 1 | bicomi | |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( ph <-> ps ) ) |