Description: Factor out the common proof skeleton of moanimv and moanim . (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 24-Dec-2018) Factor out common proof lines. (Revised by Wolf Lammen, 8-Feb-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | moanimlem.1 | ⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) | |
| moanimlem.2 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 ) | ||
| Assertion | moanimlem | ⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moanimlem.1 | ⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) | |
| 2 | moanimlem.2 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 ) | |
| 3 | 1 | biimprcd | ⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → ∃* 𝑥 𝜓 ) ) |
| 4 | nexmo | ⊢ ( ¬ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) | |
| 5 | 2 4 | nsyl5 | ⊢ ( ¬ 𝜑 → ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) |
| 6 | moan | ⊢ ( ∃* 𝑥 𝜓 → ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) | |
| 7 | 5 6 | ja | ⊢ ( ( 𝜑 → ∃* 𝑥 𝜓 ) → ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ) |
| 8 | 3 7 | impbii | ⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑥 𝜓 ) ) |