![]() |
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 28189 axpasch 28199 exatleN 38275 ps-2b 38353 3atlem1 38354 3atlem2 38355 3atlem4 38357 3atlem5 38358 3atlem6 38359 2llnjaN 38437 2llnjN 38438 4atlem12b 38482 2lplnja 38490 2lplnj 38491 dalemrea 38499 dath2 38608 lneq2at 38649 osumcllem7N 38833 cdleme26ee 39231 cdlemg35 39584 cdlemg36 39585 cdlemj1 39692 cdlemk23-3 39773 cdlemk25-3 39775 cdlemk26b-3 39776 cdlemk27-3 39778 cdlemk28-3 39779 cdleml3N 39849 iscnrm3llem2 47583 |
Copyright terms: Public domain | W3C validator |