![]() |
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 1209 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
2 | 1 | 3ad2ant1 1132 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: ax5seglem3 28961 3atlem1 39466 3atlem2 39467 3atlem5 39470 2llnjaN 39549 4atlem11b 39591 4atlem12b 39594 lplncvrlvol2 39598 dalemtea 39613 dath2 39720 cdlemblem 39776 dalawlem1 39854 lhpexle3lem 39994 4atexlemex6 40057 cdleme22f2 40330 cdleme22g 40331 cdlemg7aN 40608 cdlemg34 40695 cdlemj1 40804 cdlemk23-3 40885 cdlemk25-3 40887 cdlemk26b-3 40888 |
Copyright terms: Public domain | W3C validator |