Description: Strengthening hbnt by replacing its consequent with a biconditional. See also hbntg and hbntal . (Contributed by BJ, 20-Oct-2019) Proved from bj-19.9htbi . (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-hbntbi | |- ( A. x ( ph -> A. x ph ) -> ( -. ph <-> A. x -. ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-19.9htbi | |- ( A. x ( ph -> A. x ph ) -> ( E. x ph <-> ph ) ) |
|
| 2 | 1 | bicomd | |- ( A. x ( ph -> A. x ph ) -> ( ph <-> E. x ph ) ) |
| 3 | 2 | notbid | |- ( A. x ( ph -> A. x ph ) -> ( -. ph <-> -. E. x ph ) ) |
| 4 | alnex | |- ( A. x -. ph <-> -. E. x ph ) |
|
| 5 | 3 4 | bitr4di | |- ( A. x ( ph -> A. x ph ) -> ( -. ph <-> A. x -. ph ) ) |