![]() |
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 763, 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 8787 lejoin1 18341 lemeet1 18355 reldir 18556 gexdvdsi 19492 lmhmlmod1 20788 pi1cpbl 24791 oppne1 28259 trgcopyeulem 28323 dfcgra2 28348 subupgr 28811 3trlond 29693 3pthond 29695 3spthond 29697 grpolid 30036 mgcf1 32425 mgccole1 32427 mgcmnt1 32429 mgcmnt2 32430 mgcf1olem1 32438 mgcf1olem2 32439 mgcf1o 32440 mfsdisj 34839 linethru 35429 rngoablo 37079 fourierdlem37 45158 fourierdlem48 45168 fourierdlem93 45213 fourierdlem94 45214 fourierdlem104 45224 fourierdlem112 45232 fourierdlem113 45233 dmmeasal 45466 meaf 45467 meaiuninclem 45494 omef 45510 ome0 45511 omedm 45513 hspmbllem3 45642 |
Copyright terms: Public domain | W3C validator |