![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp123 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp123 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp23 1209 | . 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 axpasch 28179 exatleN 38213 ps-2b 38291 3atlem1 38292 3atlem2 38293 3atlem4 38295 3atlem5 38296 3atlem6 38297 2llnjaN 38375 2llnjN 38376 4atlem12b 38420 2lplnja 38428 2lplnj 38429 dalemrea 38437 dath2 38546 lneq2at 38587 osumcllem7N 38771 cdleme26ee 39169 cdlemg35 39522 cdlemg36 39523 cdlemj1 39630 cdlemk23-3 39711 cdlemk25-3 39713 cdlemk26b-3 39714 cdlemk27-3 39716 cdlemk28-3 39717 cdleml3N 39787 iscnrm3llem2 47485 |
Copyright terms: Public domain | W3C validator |