![]() |
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 783, 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 490 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simpld 490 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: erinxp 8086 lejoin1 17365 lemeet1 17379 reldir 17586 gexdvdsi 18349 lmhmlmod1 19392 pi1cpbl 23213 oppne1 26050 trgcopyeulem 26114 dfcgra2 26138 subupgr 26584 3trlond 27538 3pthond 27540 3spthond 27542 grpolid 27915 mfsdisj 31982 linethru 32788 rngoablo 34242 fourierdlem37 41148 fourierdlem48 41158 fourierdlem93 41203 fourierdlem94 41204 fourierdlem104 41214 fourierdlem112 41222 fourierdlem113 41223 ismea 41452 dmmeasal 41453 meaf 41454 meaiuninclem 41481 omef 41497 ome0 41498 omedm 41500 hspmbllem3 41629 |
Copyright terms: Public domain | W3C validator |