![]() |
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 496 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
3 | 2 | simpld 495 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 |
This theorem is referenced by: fpwwe2lem5 10529 fpwwe2lem6 10530 fpwwe2lem8 10532 canthnumlem 10542 canthp1lem2 10547 latcl2 18279 clatlem 18345 dirtr 18445 srglz 19892 lmodvsass 20294 lmghm 20439 evlssca 21445 mircgr 27444 dfcgra2 27617 mgcmnt1d 31699 mgcmnt2d 31700 mgcf1o 31705 ssmxidllem 32076 ssmxidl 32077 maxsta 33976 lbioc 43646 icccncfext 44023 stoweidlem37 44173 fourierdlem41 44284 fourierdlem48 44290 fourierdlem49 44291 fourierdlem74 44316 fourierdlem75 44317 salgencl 44468 salgenuni 44473 issalgend 44474 smfaddlem1 44899 |
Copyright terms: Public domain | W3C validator |