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 474 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simprd 478 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: dfcgra2 25521 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 fourierdlem48 39047 fourierdlem76 39075 fourierdlem80 39079 fourierdlem93 39092 fourierdlem94 39093 fourierdlem104 39103 fourierdlem113 39112 ismea 39344 mea0 39347 meaiunlelem 39361 meaiuninclem 39373 omessle 39388 omedm 39389 carageniuncllem2 39412 hspmbllem3 39518 isclwwlksng 41196 |
Copyright terms: Public domain | W3C validator |