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 734 | 1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: ghmcmn 18952 ustuqtop2 22851 ustuqtop4 22853 cnheibor 23559 miriso 26456 f1otrg 26657 txomap 31098 pstmxmet 31137 omssubadd 31558 signstfvneq0 31842 iunconnlem2 41289 suplesup 41627 limcleqr 41945 0ellimcdiv 41950 limclner 41952 fourierdlem51 42462 smflimlem2 43068 |
Copyright terms: Public domain | W3C validator |