![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp133 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp133 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp33 1269 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | 3ad2ant1 1164 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1108 |
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 199 df-an 386 df-3an 1110 |
This theorem is referenced by: tsmsxp 22286 ax5seglem3 26168 exatleN 35425 3atlem1 35504 3atlem2 35505 3atlem6 35509 4atlem11b 35629 4atlem12b 35632 lplncvrlvol2 35636 dalemuea 35652 dath2 35758 4atexlemex6 36095 cdleme22f2 36368 cdleme22g 36369 cdlemg7aN 36646 cdlemg31c 36720 cdlemg36 36735 cdlemj1 36842 cdlemj2 36843 cdlemk23-3 36923 cdlemk26b-3 36926 |
Copyright terms: Public domain | W3C validator |