![]() |
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 1207 | . 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 axpasch 28971 exatleN 39387 ps-2b 39465 3atlem1 39466 3atlem2 39467 3atlem4 39469 3atlem5 39470 3atlem6 39471 2llnjaN 39549 2llnjN 39550 4atlem12b 39594 2lplnja 39602 2lplnj 39603 dalemrea 39611 dath2 39720 lneq2at 39761 osumcllem7N 39945 cdleme26ee 40343 cdlemg35 40696 cdlemg36 40697 cdlemj1 40804 cdlemk23-3 40885 cdlemk25-3 40887 cdlemk26b-3 40888 cdlemk27-3 40890 cdlemk28-3 40891 cdleml3N 40961 iscnrm3llem2 48747 |
Copyright terms: Public domain | W3C validator |