![]() |
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 487 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simprd 488 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 |
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 388 |
This theorem is referenced by: erinxp 8163 fpwwe2lem6 9847 fpwwe2lem7 9848 fpwwe2lem9 9850 lejoin2 17471 lemeet2 17485 dirdm 17692 dirref 17693 lmhmlmod2 19516 pi1cpbl 23341 pntlemr 25870 oppne2 26220 dfcgra2 26308 mtyf2 32258 ioodvbdlimc1lem2 41593 ioodvbdlimc2lem 41595 fourierdlem48 41816 fourierdlem76 41844 fourierdlem80 41848 fourierdlem93 41861 fourierdlem94 41862 fourierdlem104 41872 fourierdlem113 41881 mea0 42113 meaiunlelem 42127 meaiuninclem 42139 omessle 42157 omedm 42158 carageniuncllem2 42181 hspmbllem3 42287 |
Copyright terms: Public domain | W3C validator |