| 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 1087 |
| 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 1089 |
| This theorem is referenced by: ax5seglem3 28946 axpasch 28956 exatleN 39406 ps-2b 39484 3atlem1 39485 3atlem2 39486 3atlem4 39488 3atlem5 39489 3atlem6 39490 2llnjaN 39568 2llnjN 39569 4atlem12b 39613 2lplnja 39621 2lplnj 39622 dalemrea 39630 dath2 39739 lneq2at 39780 osumcllem7N 39964 cdleme26ee 40362 cdlemg35 40715 cdlemg36 40716 cdlemj1 40823 cdlemk23-3 40904 cdlemk25-3 40906 cdlemk26b-3 40907 cdlemk27-3 40909 cdlemk28-3 40910 cdleml3N 40980 iscnrm3llem2 48847 |
| Copyright terms: Public domain | W3C validator |