| 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 207 df-an 396 |
| This theorem is referenced by: ornld 1062 2reu5 3764 intab 4978 dfac5 10169 grothpw 10866 grothpwex 10867 gcdcllem1 16536 gsmsymgreqlem2 19449 neindisj2 23131 tx1stc 23658 ufinffr 23937 ucnima 24290 frgr2wwlk1 30348 r19.29ffa 32490 prmidl2 33469 fmcncfil 33930 sgn3da 34544 bnj605 34921 bnj594 34926 bnj1174 35017 itg2gt0cn 37682 unirep 37721 ispridl2 38045 cnf1dd 38097 faosnf0.11b 43440 dfsucon 43536 unisnALT 44946 ax6e2ndALT 44950 ssinc 45092 ssdec 45093 fmul01 45595 dvnmptconst 45956 dvnmul 45958 2reu8i 47125 iccpartnel 47425 stgoldbwt 47763 sbgoldbalt 47768 bgoldbtbnd 47796 |
| Copyright terms: Public domain | W3C validator |