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 1213 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | 3ad2ant1 1135 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: tsmsxp 23065 ax5seglem3 27035 exatleN 37168 3atlem1 37247 3atlem2 37248 3atlem6 37252 4atlem11b 37372 4atlem12b 37375 lplncvrlvol2 37379 dalemuea 37395 dath2 37501 4atexlemex6 37838 cdleme22f2 38111 cdleme22g 38112 cdlemg7aN 38389 cdlemg31c 38463 cdlemg36 38478 cdlemj1 38585 cdlemj2 38586 cdlemk23-3 38666 cdlemk26b-3 38669 |
Copyright terms: Public domain | W3C validator |