| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp21r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp21r | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1r 1199 | . 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: modexp 14277 segconeu 36012 4atlem10 39608 lplncvrlvol2 39617 4atex 40078 4atex2-0cOLDN 40082 cdleme0moN 40227 cdleme16e 40284 cdleme17d1 40291 cdleme18d 40297 cdleme19d 40308 cdleme20f 40316 cdleme20g 40317 cdleme21ct 40331 cdleme22aa 40341 cdleme22cN 40344 cdleme22d 40345 cdleme22e 40346 cdleme22eALTN 40347 cdleme26e 40361 cdleme32e 40447 cdleme32f 40448 cdlemg4 40619 cdlemg18d 40683 cdlemg18 40684 cdlemg19a 40685 cdlemg19 40686 cdlemg21 40688 cdlemg33b0 40703 cdlemk5 40838 cdlemk6 40839 cdlemk7 40850 cdlemk11 40851 cdlemk12 40852 cdlemk21N 40875 cdlemk20 40876 cdlemk28-3 40910 cdlemk34 40912 cdlemkfid3N 40927 cdlemk55u1 40967 |
| Copyright terms: Public domain | W3C validator |