![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm3.35 | Structured version Visualization version GIF version |
Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 42. (Contributed by NM, 14-Dec-2002.) |
Ref | Expression |
---|---|
pm3.35 | ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.27 42 | . 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
2 | 1 | imp 410 | 1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: ornld 1057 2reu5 3697 intab 4868 dfac5 9539 grothpw 10237 grothpwex 10238 gcdcllem1 15838 gsmsymgreqlem2 18551 neindisj2 21728 tx1stc 22255 ufinffr 22534 ucnima 22887 frgr2wwlk1 28114 r19.29ffa 30244 prmidl2 31024 fmcncfil 31284 sgn3da 31909 bnj605 32289 bnj594 32294 bnj1174 32385 itg2gt0cn 35112 unirep 35151 ispridl2 35476 cnf1dd 35528 dfsucon 40231 unisnALT 41632 ax6e2ndALT 41636 ssinc 41723 ssdec 41724 fmul01 42222 dvnmptconst 42583 dvnmul 42585 2reu8i 43669 iccpartnel 43955 stgoldbwt 44294 sbgoldbalt 44299 bgoldbtbnd 44327 |
Copyright terms: Public domain | W3C validator |