Description: An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim in dvelimdf to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-nfimf1 | |- ( A. x ph -> ( F/ x ( ph -> ps ) <-> F/ x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | |- F/ x A. x ph |
|
| 2 | pm5.5 | |- ( ph -> ( ( ph -> ps ) <-> ps ) ) |
|
| 3 | 2 | sps | |- ( A. x ph -> ( ( ph -> ps ) <-> ps ) ) |
| 4 | 1 3 | nfbidf | |- ( A. x ph -> ( F/ x ( ph -> ps ) <-> F/ x ps ) ) |