Description: Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | eel11111.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| eel11111.2 | ⊢ ( 𝜑 → 𝜒 ) | ||
| eel11111.3 | ⊢ ( 𝜑 → 𝜃 ) | ||
| eel11111.4 | ⊢ ( 𝜑 → 𝜏 ) | ||
| eel11111.5 | ⊢ ( 𝜑 → 𝜂 ) | ||
| eel11111.6 | ⊢ ( ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) → 𝜁 ) | ||
| Assertion | eel11111 | ⊢ ( 𝜑 → 𝜁 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eel11111.1 | ⊢ ( 𝜑 → 𝜓 ) | |
| 2 | eel11111.2 | ⊢ ( 𝜑 → 𝜒 ) | |
| 3 | eel11111.3 | ⊢ ( 𝜑 → 𝜃 ) | |
| 4 | eel11111.4 | ⊢ ( 𝜑 → 𝜏 ) | |
| 5 | eel11111.5 | ⊢ ( 𝜑 → 𝜂 ) | |
| 6 | eel11111.6 | ⊢ ( ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) → 𝜁 ) | |
| 7 | 6 | exp41 | ⊢ ( ( 𝜓 ∧ 𝜒 ) → ( 𝜃 → ( 𝜏 → ( 𝜂 → 𝜁 ) ) ) ) |
| 8 | 7 | ex | ⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏 → ( 𝜂 → 𝜁 ) ) ) ) ) |
| 9 | 1 2 3 8 | syl3c | ⊢ ( 𝜑 → ( 𝜏 → ( 𝜂 → 𝜁 ) ) ) |
| 10 | 4 5 9 | mp2d | ⊢ ( 𝜑 → 𝜁 ) |