![]() |
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 1178 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1115 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: ps-2c 36057 cdlema1N 36320 cdlemednpq 36828 cdleme19e 36836 cdleme20h 36845 cdleme20j 36847 cdleme20l2 36850 cdleme20m 36852 cdleme22a 36869 cdleme22cN 36871 cdleme22f2 36876 cdleme26f2ALTN 36893 cdleme37m 36991 cdlemg12f 37177 cdlemg12g 37178 cdlemg12 37179 cdlemg28a 37222 cdlemg29 37234 cdlemg33a 37235 cdlemg36 37243 cdlemk16a 37385 cdlemk21-2N 37420 cdlemk54 37487 dihord10 37752 |
Copyright terms: Public domain | W3C validator |