| 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 1203 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant2 1135 | 1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: ax5seglem6 28949 lshpkrlem5 39115 lplnexllnN 39566 4atexlemutvt 40056 cdlemc5 40197 cdlemd2 40201 cdleme0moN 40227 cdleme3h 40237 cdleme5 40242 cdleme9 40255 cdleme11l 40271 cdleme14 40275 cdleme15c 40278 cdleme16b 40281 cdleme16d 40283 cdleme16e 40284 cdlemednpq 40301 cdleme20bN 40312 cdleme20j 40320 cdleme20l2 40323 cdleme20l 40324 cdleme22cN 40344 cdleme22d 40345 cdleme22e 40346 cdleme22f 40348 cdleme26fALTN 40364 cdleme26f 40365 cdleme26f2ALTN 40366 cdleme26f2 40367 cdleme27a 40369 cdleme32b 40444 cdleme32d 40446 cdleme32f 40448 cdleme39n 40468 cdleme40n 40470 cdlemg2fv2 40602 cdlemg17h 40670 cdlemg27b 40698 cdlemg28b 40705 cdlemg28 40706 cdlemg29 40707 cdlemg33a 40708 cdlemg33d 40711 cdlemk7u-2N 40890 cdlemk11u-2N 40891 cdlemk12u-2N 40892 cdlemk26-3 40908 cdlemk27-3 40909 cdlemkfid3N 40927 cdlemn11c 41211 |
| Copyright terms: Public domain | W3C validator |