| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp3rr | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp3rr | ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprr 773 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant3 1136 | 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: poxp3 8175 omeu 8623 ntrivcvgmul 15938 tsmsxp 24163 tgqioo 24821 ovolunlem2 25533 plyadd 26256 plymul 26257 coeeu 26264 nosupbnd1lem2 27754 noinfbnd1lem2 27769 tghilberti2 28646 cvmlift2lem10 35317 btwnconn1lem1 36088 lplnexllnN 39566 2llnjN 39569 4atlem12b 39613 lplncvrlvol2 39617 lncmp 39785 cdlema2N 39794 cdleme11a 40262 cdleme24 40354 cdleme28 40375 cdlemefr29bpre0N 40408 cdlemefr29clN 40409 cdlemefr32fvaN 40411 cdlemefr32fva1 40412 cdlemefs29bpre0N 40418 cdlemefs29bpre1N 40419 cdlemefs29cpre1N 40420 cdlemefs29clN 40421 cdlemefs32fvaN 40424 cdlemefs32fva1 40425 cdleme36m 40463 cdleme17d3 40498 cdlemg36 40716 cdlemj3 40825 cdlemkid1 40924 cdlemk19ylem 40932 cdlemk19xlem 40944 dihlsscpre 41236 dihord4 41260 dihmeetlem1N 41292 dihatlat 41336 jm2.27 43020 |
| Copyright terms: Public domain | W3C validator |