Description: Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011) (Proof shortened by Wolf Lammen, 27-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nanbi1 | |- ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imbi1 | |- ( ( ph <-> ps ) -> ( ( ph -> -. ch ) <-> ( ps -> -. ch ) ) ) |
|
| 2 | dfnan2 | |- ( ( ph -/\ ch ) <-> ( ph -> -. ch ) ) |
|
| 3 | dfnan2 | |- ( ( ps -/\ ch ) <-> ( ps -> -. ch ) ) |
|
| 4 | 1 2 3 | 3bitr4g | |- ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) ) |