![]() |
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 770 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1135 | 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 8641 hashbclem 14501 ntrivcvgmul 15950 tsmsxp 24184 tgqioo 24841 ovolunlem2 25552 plyadd 26276 plymul 26277 coeeu 26284 nosupbnd1lem2 27772 noinfbnd1lem2 27787 tghilberti2 28664 cvmlift2lem10 35280 btwnconn1lem1 36051 btwnconn1lem2 36052 btwnconn1lem12 36062 lplnexllnN 39521 2llnjN 39524 4atlem12b 39568 lplncvrlvol2 39572 lncmp 39740 cdlema2N 39749 cdlemc2 40149 cdleme11a 40217 cdleme22eALTN 40302 cdleme24 40309 cdleme27a 40324 cdleme27N 40326 cdleme28 40330 cdlemefs29bpre0N 40373 cdlemefs29bpre1N 40374 cdlemefs29cpre1N 40375 cdlemefs29clN 40376 cdlemefs32fvaN 40379 cdlemefs32fva1 40380 cdleme36m 40418 cdleme39a 40422 cdleme17d3 40453 cdleme50trn2 40508 cdlemg36 40671 cdlemj3 40780 cdlemkfid1N 40878 cdlemkid1 40879 cdlemk19ylem 40887 cdlemk19xlem 40899 dihlsscpre 41191 dihord4 41215 dihatlat 41291 mapdh9a 41746 jm2.27 42965 |
Copyright terms: Public domain | W3C validator |