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 1207 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | 3ad2ant1 1129 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 |
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 df-3an 1085 |
This theorem is referenced by: tsmsxp 22765 ax5seglem3 26719 exatleN 36542 3atlem1 36621 3atlem2 36622 3atlem6 36626 4atlem11b 36746 4atlem12b 36749 lplncvrlvol2 36753 dalemuea 36769 dath2 36875 4atexlemex6 37212 cdleme22f2 37485 cdleme22g 37486 cdlemg7aN 37763 cdlemg31c 37837 cdlemg36 37852 cdlemj1 37959 cdlemj2 37960 cdlemk23-3 38040 cdlemk26b-3 38043 |
Copyright terms: Public domain | W3C validator |