![]() |
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 735 | 1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: ghmcmn 19699 ustuqtop2 23747 ustuqtop4 23749 cnheibor 24471 miriso 27952 f1otrg 28153 txomap 32845 pstmxmet 32908 omssubadd 33330 signstfvneq0 33614 iunconnlem2 43744 suplesup 44097 limcleqr 44408 0ellimcdiv 44413 limclner 44415 fourierdlem51 44921 smflimlem2 45536 |
Copyright terms: Public domain | W3C validator |