![]() |
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 1197 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1134 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: ps-2c 39511 cdlema1N 39774 cdlemednpq 40282 cdleme19e 40290 cdleme20h 40299 cdleme20j 40301 cdleme20l2 40304 cdleme20m 40306 cdleme22a 40323 cdleme22cN 40325 cdleme22f2 40330 cdleme26f2ALTN 40347 cdleme37m 40445 cdlemg12f 40631 cdlemg12g 40632 cdlemg12 40633 cdlemg28a 40676 cdlemg29 40688 cdlemg33a 40689 cdlemg36 40697 cdlemk16a 40839 cdlemk21-2N 40874 cdlemk54 40941 dihord10 41206 |
Copyright terms: Public domain | W3C validator |