![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.53 | Structured version Visualization version Unicode 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 372 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 198 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: jaoi 381 orel1 384 pm2.63 797 pm2.8 861 19.30 1744 19.33b 1748 soxp 6909 iccpnfcnv 21972 elpreq 28157 xlt2addrd 28338 xrge0iifcnv 28739 expdioph 35878 pm10.57 36720 vk15.4j 36885 vk15.4jVD 37311 sineq0ALT 37334 disjinfi 37468 xrlexaddrp 37575 sumnnodd 37710 stoweidlem39 37900 dirkercncflem2 37966 fourierdlem101 38071 fourierswlem 38094 salexct 38193 xnn0nnn0pnf 39085 |
Copyright terms: Public domain | W3C validator |