**Description:** Infer an equivalence from an implication and its converse. Inference
associated with impbi . (Contributed by NM, 29-Dec-1992)

Ref | Expression | ||
---|---|---|---|

Hypotheses | impbii.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

impbii.2 | $${\u22a2}{\psi}\to {\phi}$$ | ||

Assertion | impbii | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | impbii.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

2 | impbii.2 | $${\u22a2}{\psi}\to {\phi}$$ | |

3 | impbi | $${\u22a2}\left({\phi}\to {\psi}\right)\to \left(\left({\psi}\to {\phi}\right)\to \left({\phi}\leftrightarrow {\psi}\right)\right)$$ | |

4 | 1 2 3 | mp2 | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ |