![]() |
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 846 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | 1 | biimpi 215 | 1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 845 |
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-or 846 |
This theorem is referenced by: jaoi 855 mtord 878 orel1 887 orim12dALT 910 biorfi 937 pm2.63 939 pm2.8 971 19.30 1884 19.33b 1888 r19.30 3121 r19.30OLD 3122 soxp 8057 xnn0nnn0pnf 12494 iccpnfcnv 24291 elpreq 31343 xlt2addrd 31546 xrge0iifcnv 32383 expdioph 41285 pm10.57 42593 vk15.4j 42752 vk15.4jVD 43138 sineq0ALT 43161 xrnmnfpnf 43235 disjinfi 43348 xrlexaddrp 43522 xrred 43535 xrnpnfmnf 43646 sumnnodd 43803 stoweidlem39 44212 dirkercncflem2 44277 fourierdlem101 44380 fourierswlem 44403 salexct 44507 |
Copyright terms: Public domain | W3C validator |