| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simprld | Structured version Visualization version GIF version | ||
| Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| Ref | Expression |
|---|---|
| simprld.1 | ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
| Ref | Expression |
|---|---|
| simprld | ⊢ (𝜑 → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprld.1 | . . 3 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) | |
| 2 | 1 | simprd 495 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
| 3 | 2 | simpld 494 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 canthnumlem 10688 canthp1lem2 10693 latcl2 18481 clatlem 18547 dirtr 18647 srglz 20205 lmodvsass 20885 lmghm 21030 evlssca 22113 mircgr 28665 dfcgra2 28838 mgcmnt1d 32987 mgcmnt2d 32988 mgcf1o 32993 ssmxidllem 33501 ssmxidl 33502 maxsta 35559 lbioc 45526 icccncfext 45902 stoweidlem37 46052 fourierdlem41 46163 fourierdlem48 46169 fourierdlem49 46170 fourierdlem74 46195 fourierdlem75 46196 salgencl 46347 salgenuni 46352 issalgend 46353 smfaddlem1 46778 |
| Copyright terms: Public domain | W3C validator |