| 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 771 | . 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: omeu 8623 hashbclem 14491 ntrivcvgmul 15938 tsmsxp 24163 tgqioo 24821 ovolunlem2 25533 plyadd 26256 plymul 26257 coeeu 26264 nosupbnd1lem2 27754 noinfbnd1lem2 27769 tghilberti2 28646 cvmlift2lem10 35317 btwnconn1lem1 36088 btwnconn1lem2 36089 btwnconn1lem12 36099 lplnexllnN 39566 2llnjN 39569 4atlem12b 39613 lplncvrlvol2 39617 lncmp 39785 cdlema2N 39794 cdlemc2 40194 cdleme11a 40262 cdleme22eALTN 40347 cdleme24 40354 cdleme27a 40369 cdleme27N 40371 cdleme28 40375 cdlemefs29bpre0N 40418 cdlemefs29bpre1N 40419 cdlemefs29cpre1N 40420 cdlemefs29clN 40421 cdlemefs32fvaN 40424 cdlemefs32fva1 40425 cdleme36m 40463 cdleme39a 40467 cdleme17d3 40498 cdleme50trn2 40553 cdlemg36 40716 cdlemj3 40825 cdlemkfid1N 40923 cdlemkid1 40924 cdlemk19ylem 40932 cdlemk19xlem 40944 dihlsscpre 41236 dihord4 41260 dihatlat 41336 mapdh9a 41791 jm2.27 43020 |
| Copyright terms: Public domain | W3C validator |