Description: Strengthening 19.9ht by replacing its succedent with a biconditional ( 19.9t does have a biconditional succedent). This propagates. (Contributed by BJ, 20-Oct-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-19.9htbi | |- ( A. x ( ph -> A. x ph ) -> ( E. x ph <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.9ht | |- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) ) |
|
| 2 | 19.8a | |- ( ph -> E. x ph ) |
|
| 3 | 1 2 | impbid1 | |- ( A. x ( ph -> A. x ph ) -> ( E. x ph <-> ph ) ) |