![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > olc | GIF version |
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
olc | ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ ((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) | |
2 | jaob 631 | . . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))) | |
3 | 1, 2 | mpbi 133 | . 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))) |
4 | 3 | simpri 106 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∨ wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm1.4 646 olci 651 pm2.07 656 pm2.46 658 biorf 663 pm1.5 682 pm2.41 693 pm3.48 699 ordi 729 andi 731 pm4.72 736 pm2.54dc 790 oibabs 800 pm4.78i 808 pm2.85dc 811 dcor 843 dedlemb 877 xoranor 1268 19.33 1373 hbor 1438 nford 1459 19.30dc 1518 19.43 1519 19.32r 1570 euor2 1958 mooran2 1973 r19.32r 2457 undif3ss 3198 undif4 3284 issod 4056 onsucelsucexmid 4255 sucprcreg 4273 0elnn 4340 acexmidlemph 5505 nntri3or 6072 swoord1 6135 swoord2 6136 addlocprlem 6633 nqprloc 6643 apreap 7578 zletric 8289 zlelttric 8290 zmulcl 8297 zdceq 8316 zdcle 8317 zdclt 8318 nn0lt2 8322 elnn1uz2 8544 mnflt 8704 mnfltpnf 8706 xrltso 8717 fzdcel 8904 fzm1 8962 qletric 9099 qlelttric 9100 qdceq 9102 |
Copyright terms: Public domain | W3C validator |