![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplld | Structured version Visualization version GIF version |
Description: Deduction form of simpll 765, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
simplld.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
Ref | Expression |
---|---|
simplld | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplld.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
2 | 1 | simpld 493 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simpld 493 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: erinxp 8810 lejoin1 18379 lemeet1 18393 reldir 18594 gexdvdsi 19550 lmhmlmod1 20930 pi1cpbl 25015 oppne1 28617 trgcopyeulem 28681 dfcgra2 28706 subupgr 29172 3trlond 30055 3pthond 30057 3spthond 30059 grpolid 30398 mgcf1 32804 mgccole1 32806 mgcmnt1 32808 mgcmnt2 32809 mgcf1olem1 32817 mgcf1olem2 32818 mgcf1o 32819 erlcl1 33050 erler 33055 mfsdisj 35288 linethru 35877 rngoablo 37509 fourierdlem37 45667 fourierdlem48 45677 fourierdlem93 45722 fourierdlem94 45723 fourierdlem104 45733 fourierdlem112 45741 fourierdlem113 45742 dmmeasal 45975 meaf 45976 meaiuninclem 46003 omef 46019 ome0 46020 omedm 46022 hspmbllem3 46151 |
Copyright terms: Public domain | W3C validator |