**Description:** Two truths are equivalent. (Contributed by NM, 18-Aug-1993)

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

Hypotheses | 2th.1 | $${\u22a2}{\phi}$$ | |

2th.2 | $${\u22a2}{\psi}$$ | ||

Assertion | 2th | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ |

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

1 | 2th.1 | $${\u22a2}{\phi}$$ | |

2 | 2th.2 | $${\u22a2}{\psi}$$ | |

3 | 2 | a1i | $${\u22a2}{\phi}\to {\psi}$$ |

4 | 1 | a1i | $${\u22a2}{\psi}\to {\phi}$$ |

5 | 3 4 | impbii | $${\u22a2}{\phi}\leftrightarrow {\psi}$$ |