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 769 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant3 1127 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: omeu 8200 ntrivcvgmul 15246 tsmsxp 22690 tgqioo 23335 ovolunlem2 24026 plyadd 24734 plymul 24735 coeeu 24742 tghilberti2 26351 cvmlift2lem10 32456 nosupbnd1lem2 33106 btwnconn1lem1 33445 lplnexllnN 36580 2llnjN 36583 4atlem12b 36627 lplncvrlvol2 36631 lncmp 36799 cdlema2N 36808 cdleme11a 37276 cdleme24 37368 cdleme28 37389 cdlemefr29bpre0N 37422 cdlemefr29clN 37423 cdlemefr32fvaN 37425 cdlemefr32fva1 37426 cdlemefs29bpre0N 37432 cdlemefs29bpre1N 37433 cdlemefs29cpre1N 37434 cdlemefs29clN 37435 cdlemefs32fvaN 37438 cdlemefs32fva1 37439 cdleme36m 37477 cdleme17d3 37512 cdlemg36 37730 cdlemj3 37839 cdlemkid1 37938 cdlemk19ylem 37946 cdlemk19xlem 37958 dihlsscpre 38250 dihord4 38274 dihmeetlem1N 38306 dihatlat 38350 jm2.27 39483 |
Copyright terms: Public domain | W3C validator |