![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp132 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp132 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1211 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
2 | 1 | 3ad2ant1 1134 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 df-3an 1090 |
This theorem is referenced by: ax5seglem3 28169 3atlem1 38292 3atlem2 38293 3atlem5 38296 2llnjaN 38375 4atlem11b 38417 4atlem12b 38420 lplncvrlvol2 38424 dalemtea 38439 dath2 38546 cdlemblem 38602 dalawlem1 38680 lhpexle3lem 38820 4atexlemex6 38883 cdleme22f2 39156 cdleme22g 39157 cdlemg7aN 39434 cdlemg34 39521 cdlemj1 39630 cdlemk23-3 39711 cdlemk25-3 39713 cdlemk26b-3 39714 |
Copyright terms: Public domain | W3C validator |