| 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 494 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
| 3 | 2 | simprd 495 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: erinxp 8831 fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 lejoin2 18430 lemeet2 18444 dirdm 18645 dirref 18646 lmhmlmod2 21031 pi1cpbl 25077 pntlemr 27646 oppne2 28750 dfcgra2 28838 mgcf2 32979 mgccole2 32981 mgcmnt1 32982 mgcmnt2 32983 mgcf1olem1 32991 mgcf1olem2 32992 mgcf1o 32993 erlcl2 33265 erler 33269 mtyf2 35556 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 fourierdlem48 46169 fourierdlem76 46197 fourierdlem80 46201 fourierdlem93 46214 fourierdlem94 46215 fourierdlem104 46225 fourierdlem113 46234 mea0 46469 meaiunlelem 46483 meaiuninclem 46495 omessle 46513 omedm 46514 carageniuncllem2 46537 hspmbllem3 46643 uprcl5 48944 |
| Copyright terms: Public domain | W3C validator |