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 844 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | 1 | biimpi 218 | 1 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 |
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 209 df-or 844 |
This theorem is referenced by: jaoi 853 mtord 876 orel1 885 orim12dALT 908 biorfi 935 pm2.63 937 pm2.8 969 19.30 1882 19.33b 1886 r19.30 3338 soxp 7823 xnn0nnn0pnf 11981 iccpnfcnv 23548 elpreq 30290 xlt2addrd 30482 xrge0iifcnv 31176 expdioph 39640 pm10.57 40723 vk15.4j 40882 vk15.4jVD 41268 sineq0ALT 41291 xrnmnfpnf 41367 disjinfi 41474 xrlexaddrp 41640 xrred 41653 xrnpnfmnf 41771 sumnnodd 41931 stoweidlem39 42344 dirkercncflem2 42409 fourierdlem101 42512 fourierswlem 42535 salexct 42637 |
Copyright terms: Public domain | W3C validator |