![]() |
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 772, 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 497 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
3 | 2 | simprd 497 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: fpwwe2lem3 10628 uzind 12654 latcl2 18389 clatlem 18455 dirge 18556 srgrz 20030 lmodvs1 20500 lmhmsca 20641 evlsvar 21653 mirbtwn 27909 dfcgra2 28081 3trlond 29426 3pthond 29428 3spthond 29430 ssmxidllem 32589 ssmxidl 32590 axtgupdim2ALTV 33680 mvtinf 34546 rngoid 36770 rngoideu 36771 rngorn1eq 36802 rngomndo 36803 fzne2d 40846 mzpcl34 41469 icccncfext 44603 fourierdlem12 44835 fourierdlem34 44857 fourierdlem41 44864 fourierdlem48 44870 fourierdlem49 44871 fourierdlem74 44896 fourierdlem75 44897 fourierdlem76 44898 fourierdlem89 44911 fourierdlem91 44913 fourierdlem92 44914 fourierdlem94 44916 fourierdlem113 44935 sssalgen 45051 issalgend 45054 smfaddlem1 45479 |
Copyright terms: Public domain | W3C validator |