![]() |
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 845 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | 1 | biimpi 219 | 1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 844 |
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-or 845 |
This theorem is referenced by: jaoi 854 mtord 877 orel1 886 orim12dALT 909 biorfi 936 pm2.63 938 pm2.8 970 19.30 1882 19.33b 1886 r19.30 3293 soxp 7806 xnn0nnn0pnf 11968 iccpnfcnv 23549 elpreq 30302 xlt2addrd 30508 xrge0iifcnv 31286 expdioph 39964 pm10.57 41075 vk15.4j 41234 vk15.4jVD 41620 sineq0ALT 41643 xrnmnfpnf 41719 disjinfi 41820 xrlexaddrp 41984 xrred 41997 xrnpnfmnf 42114 sumnnodd 42272 stoweidlem39 42681 dirkercncflem2 42746 fourierdlem101 42849 fourierswlem 42872 salexct 42974 |
Copyright terms: Public domain | W3C validator |