![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplrd | Structured version Visualization version GIF version |
Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
simplrd.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
Ref | Expression |
---|---|
simplrd | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplrd.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
2 | 1 | simpld 496 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simprd 497 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: erinxp 8785 fpwwe2lem5 10630 fpwwe2lem6 10631 fpwwe2lem8 10633 lejoin2 18338 lemeet2 18352 dirdm 18553 dirref 18554 lmhmlmod2 20643 pi1cpbl 24560 pntlemr 27105 oppne2 27993 dfcgra2 28081 mgcf2 32159 mgccole2 32161 mgcmnt1 32162 mgcmnt2 32163 mgcf1olem1 32171 mgcf1olem2 32172 mgcf1o 32173 mtyf2 34542 ioodvbdlimc1lem2 44648 ioodvbdlimc2lem 44650 fourierdlem48 44870 fourierdlem76 44898 fourierdlem80 44902 fourierdlem93 44915 fourierdlem94 44916 fourierdlem104 44926 fourierdlem113 44935 mea0 45170 meaiunlelem 45184 meaiuninclem 45196 omessle 45214 omedm 45215 carageniuncllem2 45238 hspmbllem3 45344 |
Copyright terms: Public domain | W3C validator |