![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp3rl | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp3rl | ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 811 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1130 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 1074 |
This theorem is referenced by: omeu 7834 hashbclem 13428 ntrivcvgmul 14833 tsmsxp 22159 tgqioo 22804 ovolunlem2 23466 plyadd 24172 plymul 24173 coeeu 24180 tghilberti2 25732 cvmlift2lem10 31601 nosupbnd1lem2 32161 btwnconn1lem1 32500 btwnconn1lem2 32501 btwnconn1lem12 32511 lplnexllnN 35353 2llnjN 35356 4atlem12b 35400 lplncvrlvol2 35404 lncmp 35572 cdlema2N 35581 cdlemc2 35982 cdleme11a 36050 cdleme22eALTN 36135 cdleme24 36142 cdleme27a 36157 cdleme27N 36159 cdleme28 36163 cdlemefs29bpre0N 36206 cdlemefs29bpre1N 36207 cdlemefs29cpre1N 36208 cdlemefs29clN 36209 cdlemefs32fvaN 36212 cdlemefs32fva1 36213 cdleme36m 36251 cdleme39a 36255 cdleme17d3 36286 cdleme50trn2 36341 cdlemg36 36504 cdlemj3 36613 cdlemkfid1N 36711 cdlemkid1 36712 cdlemk19ylem 36720 cdlemk19xlem 36732 dihlsscpre 37025 dihord4 37049 dihatlat 37125 mapdh9a 37581 jm2.27 38077 |
Copyright terms: Public domain | W3C validator |