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 1200 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜒) | |
2 | 1 | 3ad2ant1 1125 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: ax5seglem3 26644 axpasch 26654 exatleN 36420 ps-2b 36498 3atlem1 36499 3atlem2 36500 3atlem4 36502 3atlem5 36503 3atlem6 36504 2llnjaN 36582 2llnjN 36583 4atlem12b 36627 2lplnja 36635 2lplnj 36636 dalemrea 36644 dath2 36753 lneq2at 36794 osumcllem7N 36978 cdleme26ee 37376 cdlemg35 37729 cdlemg36 37730 cdlemj1 37837 cdlemk23-3 37918 cdlemk25-3 37920 cdlemk26b-3 37921 cdlemk27-3 37923 cdlemk28-3 37924 cdleml3N 37994 |
Copyright terms: Public domain | W3C validator |