![]() |
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 493 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simprd 494 | 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 fpwwe2lem5 10660 fpwwe2lem6 10661 fpwwe2lem8 10663 lejoin2 18380 lemeet2 18394 dirdm 18595 dirref 18596 lmhmlmod2 20929 pi1cpbl 25015 pntlemr 27580 oppne2 28618 dfcgra2 28706 mgcf2 32805 mgccole2 32807 mgcmnt1 32808 mgcmnt2 32809 mgcf1olem1 32817 mgcf1olem2 32818 mgcf1o 32819 erlcl2 33051 erler 33055 mtyf2 35289 ioodvbdlimc1lem2 45455 ioodvbdlimc2lem 45457 fourierdlem48 45677 fourierdlem76 45705 fourierdlem80 45709 fourierdlem93 45722 fourierdlem94 45723 fourierdlem104 45733 fourierdlem113 45742 mea0 45977 meaiunlelem 45991 meaiuninclem 46003 omessle 46021 omedm 46022 carageniuncllem2 46045 hspmbllem3 46151 |
Copyright terms: Public domain | W3C validator |