![]() |
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 710 | . . 3 ⊢ (((𝜓 ∨ 𝜑) → (𝜓 ∨ 𝜑)) ↔ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑)))) | |
3 | 1, 2 | mpbi 145 | . 2 ⊢ ((𝜓 → (𝜓 ∨ 𝜑)) ∧ (𝜑 → (𝜓 ∨ 𝜑))) |
4 | 3 | simpri 113 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∨ wo 708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: oibabs 714 pm1.4 727 olci 732 pm2.07 737 pm2.46 739 biorf 744 pm1.5 765 pm2.41 776 pm4.78i 782 pm3.48 785 ordi 816 andi 818 pm4.72 827 stdcn 847 pm2.54dc 891 pm2.85dc 905 dcor 935 dedlemb 970 xoranor 1377 19.33 1484 hbor 1546 nford 1567 19.30dc 1627 19.43 1628 19.32r 1680 euor2 2084 mooran2 2099 r19.32r 2623 undif3ss 3398 undif4 3487 issod 4321 onsucelsucexmid 4531 sucprcreg 4550 0elnn 4620 acexmidlemph 5871 nntri3or 6497 swoord1 6567 swoord2 6568 exmidaclem 7210 exmidontri2or 7245 addlocprlem 7537 nqprloc 7547 apreap 8547 zletric 9300 zlelttric 9301 zmulcl 9309 zdceq 9331 zdcle 9332 zdclt 9333 nn0lt2 9337 elnn1uz2 9610 mnflt 9786 mnfltpnf 9788 xrltso 9799 fzdcel 10043 fzm1 10103 qletric 10247 qlelttric 10248 qdceq 10250 qsqeqor 10634 nn0o1gt2 11913 prm23lt5 12266 bj-fadc 14694 decidin 14737 triap 14966 tridceq 14993 |
Copyright terms: Public domain | W3C validator |