Description: Theorem 19.29 of Margaris p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | r19.29imd.1 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) | |
| r19.29imd.2 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ) | ||
| Assertion | r19.29imd | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r19.29imd.1 | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) | |
| 2 | r19.29imd.2 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ) | |
| 3 | r19.29r | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ ( 𝜓 → 𝜒 ) ) ) | |
| 4 | 1 2 3 | syl2anc | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ ( 𝜓 → 𝜒 ) ) ) |
| 5 | abai | ⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ ( 𝜓 → 𝜒 ) ) ) | |
| 6 | 5 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ ( 𝜓 → 𝜒 ) ) ) |
| 7 | 4 6 | sylibr | ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) ) |