![]() |
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 1241 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1130 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: ps-2c 35317 cdlema1N 35580 cdlemednpq 36089 cdleme19e 36097 cdleme20h 36106 cdleme20j 36108 cdleme20l2 36111 cdleme20m 36113 cdleme22a 36130 cdleme22cN 36132 cdleme22f2 36137 cdleme26f2ALTN 36154 cdleme37m 36252 cdlemg12f 36438 cdlemg12g 36439 cdlemg12 36440 cdlemg28a 36483 cdlemg29 36495 cdlemg33a 36496 cdlemg36 36504 cdlemk16a 36646 cdlemk21-2N 36681 cdlemk54 36748 dihord10 37014 |
Copyright terms: Public domain | W3C validator |