| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp22r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp22r | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp2r 1201 | . 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: frrlem10 8320 ttrclselem2 9766 ax5seglem6 28949 segconeu 36012 3atlem2 39486 lplnexllnN 39566 lplncvrlvol2 39617 4atex 40078 cdleme3g 40236 cdleme3h 40237 cdleme11h 40268 cdleme20bN 40312 cdleme20c 40313 cdleme20f 40316 cdleme20g 40317 cdleme20j 40320 cdleme20l2 40323 cdleme20l 40324 cdleme21ct 40331 cdleme26e 40361 cdleme43fsv1snlem 40422 cdleme39n 40468 cdleme40m 40469 cdleme42k 40486 cdlemg6c 40622 cdlemg31d 40702 cdlemg33a 40708 cdlemg33c 40710 cdlemg33d 40711 cdlemg33e 40712 cdlemg33 40713 cdlemh 40819 cdlemk7u-2N 40890 cdlemk11u-2N 40891 cdlemk12u-2N 40892 cdlemk20-2N 40894 cdlemk28-3 40910 cdlemk33N 40911 cdlemk34 40912 cdlemk39 40918 cdlemkyyN 40964 |
| Copyright terms: Public domain | W3C validator |