![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp31r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp31r | ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1r 1195 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1132 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: ps-2c 39131 cdlema1N 39394 cdlemednpq 39902 cdleme19e 39910 cdleme20h 39919 cdleme20j 39921 cdleme20l2 39924 cdleme20m 39926 cdleme22a 39943 cdleme22cN 39945 cdleme22f2 39950 cdleme26f2ALTN 39967 cdleme37m 40065 cdlemg12f 40251 cdlemg12g 40252 cdlemg12 40253 cdlemg28a 40296 cdlemg29 40308 cdlemg33a 40309 cdlemg36 40317 cdlemk16a 40459 cdlemk21-2N 40494 cdlemk54 40561 dihord10 40826 |
Copyright terms: Public domain | W3C validator |