![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp121 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp121 | ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp21 1248 | . 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑) | |
2 | 1 | 3ad2ant1 1127 | 1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: ax5seglem3 26033 axpasch 26043 exatleN 35213 ps-2b 35291 3atlem1 35292 3atlem2 35293 3atlem4 35295 3atlem5 35296 3atlem6 35297 2llnjaN 35375 4atlem12b 35420 2lplnja 35428 dalempea 35435 dath2 35546 lneq2at 35587 llnexchb2 35678 dalawlem1 35680 osumcllem7N 35771 lhpexle3lem 35820 cdleme26ee 36170 cdlemg34 36522 cdlemg36 36524 cdlemj1 36631 cdlemj2 36632 cdlemk23-3 36712 cdlemk25-3 36714 cdlemk26b-3 36715 cdlemk26-3 36716 cdlemk27-3 36717 cdleml3N 36788 |
Copyright terms: Public domain | W3C validator |