![]() |
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 770, 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 495 | . 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 206 df-an 396 |
This theorem is referenced by: fpwwe2lem3 10630 uzind 12658 latcl2 18401 clatlem 18467 dirge 18568 srgrz 20112 lmodvs1 20736 lmhmsca 20878 evlsvar 21995 mirbtwn 28417 dfcgra2 28589 3trlond 29935 3pthond 29937 3spthond 29939 ssmxidllem 33095 ssmxidl 33096 axtgupdim2ALTV 34209 mvtinf 35074 rngoid 37283 rngoideu 37284 rngorn1eq 37315 rngomndo 37316 fzne2d 41362 mzpcl34 42052 icccncfext 45180 fourierdlem12 45412 fourierdlem34 45434 fourierdlem41 45441 fourierdlem48 45447 fourierdlem49 45448 fourierdlem74 45473 fourierdlem75 45474 fourierdlem76 45475 fourierdlem89 45488 fourierdlem91 45490 fourierdlem92 45491 fourierdlem94 45493 fourierdlem113 45512 sssalgen 45628 issalgend 45631 smfaddlem1 46056 |
Copyright terms: Public domain | W3C validator |