![]() |
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 667 | . . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))) | |
3 | 1, 2 | mpbi 144 | . 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))) |
4 | 3 | simpri 112 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∨ wo 665 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-io 666 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm1.4 682 olci 687 pm2.07 692 pm2.46 694 biorf 699 pm1.5 718 pm2.41 729 pm3.48 735 ordi 766 andi 768 pm4.72 773 pm2.54dc 829 oibabs 839 pm4.78i 847 pm2.85dc 850 dcor 882 dedlemb 917 xoranor 1314 19.33 1419 hbor 1484 nford 1505 19.30dc 1564 19.43 1565 19.32r 1616 euor2 2007 mooran2 2022 r19.32r 2515 undif3ss 3261 undif4 3349 issod 4155 onsucelsucexmid 4359 sucprcreg 4378 0elnn 4445 acexmidlemph 5659 nntri3or 6268 swoord1 6335 swoord2 6336 addlocprlem 7148 nqprloc 7158 apreap 8118 zletric 8848 zlelttric 8849 zmulcl 8857 zdceq 8876 zdcle 8877 zdclt 8878 nn0lt2 8882 elnn1uz2 9148 mnflt 9307 mnfltpnf 9309 xrltso 9320 fzdcel 9508 fzm1 9568 qletric 9709 qlelttric 9710 qdceq 9712 nn0o1gt2 11237 decidin 11963 |
Copyright terms: Public domain | W3C validator |