![]() |
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. (Contributed by NM, 14-Dec-2002.) |
Ref | Expression |
---|---|
pm3.35 | ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.27 42 | . 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
2 | 1 | imp 444 | 1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: ornld 976 r19.29vva 3217 2reu5 3555 intab 4657 dfac5 9139 grothpw 9838 grothpwex 9839 gcdcllem1 15421 gsmsymgreqlem2 18049 neindisj2 21127 tx1stc 21653 ufinffr 21932 ucnima 22284 frgr2wwlk1 27481 r19.29ffa 29627 fmcncfil 30284 sgn3da 30910 bnj605 31282 bnj594 31287 bnj1174 31376 bj-ssbequ2 32947 itg2gt0cn 33776 unirep 33818 ispridl2 34148 cnf1dd 34203 unisnALT 39659 ax6e2ndALT 39663 ssinc 39761 ssdec 39762 fmul01 40313 dvnmptconst 40657 dvnmul 40659 iccpartnel 41882 stgoldbwt 42172 sbgoldbalt 42177 bgoldbtbnd 42205 |
Copyright terms: Public domain | W3C validator |