Description: Alternate proof of bj-ax12v3 . Uses axc11r and axc15 instead of ax-12 . (Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ax12v3ALT | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | ⊢ ( 𝜑 → ∀ 𝑦 𝜑 ) | |
| 2 | axc11r | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) ) | |
| 3 | ala1 | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) | |
| 4 | 1 2 3 | syl56 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| 5 | 4 | a1d | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) |
| 6 | axc15 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) ) | |
| 7 | 5 6 | pm2.61i | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |