![]() |
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 811 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant3 1104 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: omeu 7710 ntrivcvgmul 14678 tsmsxp 22005 tgqioo 22650 ovolunlem2 23312 plyadd 24018 plymul 24019 coeeu 24026 tghilberti2 25578 cvmlift2lem10 31420 nosupbnd1lem2 31980 btwnconn1lem1 32319 lplnexllnN 35168 2llnjN 35171 4atlem12b 35215 lplncvrlvol2 35219 lncmp 35387 cdlema2N 35396 cdleme11a 35865 cdleme24 35957 cdleme28 35978 cdlemefr29bpre0N 36011 cdlemefr29clN 36012 cdlemefr32fvaN 36014 cdlemefr32fva1 36015 cdlemefs29bpre0N 36021 cdlemefs29bpre1N 36022 cdlemefs29cpre1N 36023 cdlemefs29clN 36024 cdlemefs32fvaN 36027 cdlemefs32fva1 36028 cdleme36m 36066 cdleme17d3 36101 cdlemg36 36319 cdlemj3 36428 cdlemkid1 36527 cdlemk19ylem 36535 cdlemk19xlem 36547 dihlsscpre 36840 dihord4 36864 dihmeetlem1N 36896 dihatlat 36940 jm2.27 37892 |
Copyright terms: Public domain | W3C validator |