![]() |
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 770 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant3 1134 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 206 df-an 396 df-3an 1088 |
This theorem is referenced by: poxp3 8140 omeu 8589 ntrivcvgmul 15853 tsmsxp 23880 tgqioo 24537 ovolunlem2 25248 plyadd 25967 plymul 25968 coeeu 25975 nosupbnd1lem2 27449 noinfbnd1lem2 27464 tghilberti2 28157 cvmlift2lem10 34602 btwnconn1lem1 35364 lplnexllnN 38739 2llnjN 38742 4atlem12b 38786 lplncvrlvol2 38790 lncmp 38958 cdlema2N 38967 cdleme11a 39435 cdleme24 39527 cdleme28 39548 cdlemefr29bpre0N 39581 cdlemefr29clN 39582 cdlemefr32fvaN 39584 cdlemefr32fva1 39585 cdlemefs29bpre0N 39591 cdlemefs29bpre1N 39592 cdlemefs29cpre1N 39593 cdlemefs29clN 39594 cdlemefs32fvaN 39597 cdlemefs32fva1 39598 cdleme36m 39636 cdleme17d3 39671 cdlemg36 39889 cdlemj3 39998 cdlemkid1 40097 cdlemk19ylem 40105 cdlemk19xlem 40117 dihlsscpre 40409 dihord4 40433 dihmeetlem1N 40465 dihatlat 40509 jm2.27 42050 |
Copyright terms: Public domain | W3C validator |