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 406 | 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: ornld 1058 2reu5 3696 intab 4914 dfac5 9868 grothpw 10566 grothpwex 10567 gcdcllem1 16187 gsmsymgreqlem2 19020 neindisj2 22255 tx1stc 22782 ufinffr 23061 ucnima 23414 frgr2wwlk1 28672 r19.29ffa 30801 prmidl2 31595 fmcncfil 31860 sgn3da 32487 bnj605 32866 bnj594 32871 bnj1174 32962 itg2gt0cn 35811 unirep 35850 ispridl2 36175 cnf1dd 36227 dfsucon 41092 unisnALT 42499 ax6e2ndALT 42503 ssinc 42590 ssdec 42591 fmul01 43075 dvnmptconst 43436 dvnmul 43438 2reu8i 44556 iccpartnel 44842 stgoldbwt 45180 sbgoldbalt 45185 bgoldbtbnd 45213 |
Copyright terms: Public domain | W3C validator |