| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp-6l | Structured version Visualization version GIF version | ||
| Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
| Ref | Expression |
|---|---|
| simp-6l | ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
| 2 | 1 | ad6antr 736 | 1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: ghmcmn 19849 ustuqtop2 24251 ustuqtop4 24253 cnheibor 24987 miriso 28678 f1otrg 28879 txomap 33833 pstmxmet 33896 omssubadd 34302 signstfvneq0 34587 iunconnlem2 44955 suplesup 45350 limcleqr 45659 0ellimcdiv 45664 limclner 45666 fourierdlem51 46172 smflimlem2 46787 upfval 48933 |
| Copyright terms: Public domain | W3C validator |