![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simprrd | Structured version Visualization version GIF version |
Description: Deduction form of simprr 763, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
simprrd.1 | ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
Ref | Expression |
---|---|
simprrd | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprrd.1 | . . 3 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) | |
2 | 1 | simprd 491 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
3 | 2 | simprd 491 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 387 |
This theorem is referenced by: fpwwe2lem3 9790 uzind 11821 latcl2 17434 clatlem 17497 dirge 17623 srgrz 18913 lmodvs1 19283 lmhmsca 19425 evlsvar 19919 mirbtwn 26009 dfcgra2 26178 3trlond 27576 3pthond 27578 3spthond 27580 axtgupdim2OLD 31348 mvtinf 32051 rngoid 34325 rngoideu 34326 rngorn1eq 34357 rngomndo 34358 mzpcl34 38254 icccncfext 41028 fourierdlem12 41263 fourierdlem34 41285 fourierdlem41 41292 fourierdlem48 41298 fourierdlem49 41299 fourierdlem74 41324 fourierdlem75 41325 fourierdlem76 41326 fourierdlem89 41339 fourierdlem91 41341 fourierdlem92 41342 fourierdlem94 41344 fourierdlem113 41363 sssalgen 41477 issalgend 41480 smfaddlem1 41898 |
Copyright terms: Public domain | W3C validator |