![]() |
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 769 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2ant3 1135 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: omeu 8528 hashbclem 14341 ntrivcvgmul 15779 tsmsxp 23490 tgqioo 24147 ovolunlem2 24846 plyadd 25562 plymul 25563 coeeu 25570 nosupbnd1lem2 27041 noinfbnd1lem2 27056 tghilberti2 27466 cvmlift2lem10 33775 btwnconn1lem1 34639 btwnconn1lem2 34640 btwnconn1lem12 34650 lplnexllnN 37994 2llnjN 37997 4atlem12b 38041 lplncvrlvol2 38045 lncmp 38213 cdlema2N 38222 cdlemc2 38622 cdleme11a 38690 cdleme22eALTN 38775 cdleme24 38782 cdleme27a 38797 cdleme27N 38799 cdleme28 38803 cdlemefs29bpre0N 38846 cdlemefs29bpre1N 38847 cdlemefs29cpre1N 38848 cdlemefs29clN 38849 cdlemefs32fvaN 38852 cdlemefs32fva1 38853 cdleme36m 38891 cdleme39a 38895 cdleme17d3 38926 cdleme50trn2 38981 cdlemg36 39144 cdlemj3 39253 cdlemkfid1N 39351 cdlemkid1 39352 cdlemk19ylem 39360 cdlemk19xlem 39372 dihlsscpre 39664 dihord4 39688 dihatlat 39764 mapdh9a 40219 jm2.27 41270 |
Copyright terms: Public domain | W3C validator |