![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp23r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp23r | ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1202 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant2 1134 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: ax5seglem6 28057 lshpkrlem5 37787 lplnexllnN 38238 4atexlemutvt 38728 cdlemc5 38869 cdlemd2 38873 cdleme0moN 38899 cdleme3h 38909 cdleme5 38914 cdleme9 38927 cdleme11l 38943 cdleme14 38947 cdleme15c 38950 cdleme16b 38953 cdleme16d 38955 cdleme16e 38956 cdlemednpq 38973 cdleme20bN 38984 cdleme20j 38992 cdleme20l2 38995 cdleme20l 38996 cdleme22cN 39016 cdleme22d 39017 cdleme22e 39018 cdleme22f 39020 cdleme26fALTN 39036 cdleme26f 39037 cdleme26f2ALTN 39038 cdleme26f2 39039 cdleme27a 39041 cdleme32b 39116 cdleme32d 39118 cdleme32f 39120 cdleme39n 39140 cdleme40n 39142 cdlemg2fv2 39274 cdlemg17h 39342 cdlemg27b 39370 cdlemg28b 39377 cdlemg28 39378 cdlemg29 39379 cdlemg33a 39380 cdlemg33d 39383 cdlemk7u-2N 39562 cdlemk11u-2N 39563 cdlemk12u-2N 39564 cdlemk26-3 39580 cdlemk27-3 39581 cdlemkfid3N 39599 cdlemn11c 39883 |
Copyright terms: Public domain | W3C validator |