| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pm2.53 | Structured version Visualization version GIF version | ||
| Description: Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
| Ref | Expression |
|---|---|
| pm2.53 | ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-or 849 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
| 2 | 1 | biimpi 216 | 1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∨ wo 848 |
| 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-or 849 |
| This theorem is referenced by: jaoi 858 mtord 880 orel1 889 orim12dALT 912 biorfriOLD 941 pm2.63 943 pm2.8 975 19.30 1881 19.33b 1885 r19.30 3120 r19.30OLD 3121 soxp 8154 xnn0nnn0pnf 12612 iccpnfcnv 24975 nnsge1 28346 elpreq 32548 xlt2addrd 32762 xrge0iifcnv 33932 expdioph 43035 pm10.57 44390 vk15.4j 44548 vk15.4jVD 44934 sineq0ALT 44957 xrnmnfpnf 45088 disjinfi 45197 xrlexaddrp 45363 xrred 45376 xrnpnfmnf 45485 sumnnodd 45645 stoweidlem39 46054 dirkercncflem2 46119 fourierdlem101 46222 fourierswlem 46245 salexct 46349 |
| Copyright terms: Public domain | W3C validator |