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 699 | . . 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 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: oibabs 703 pm1.4 716 olci 721 pm2.07 726 pm2.46 728 biorf 733 pm1.5 754 pm2.41 765 pm4.78i 771 pm3.48 774 ordi 805 andi 807 pm4.72 812 stdcn 832 pm2.54dc 876 pm2.85dc 890 dcor 919 dedlemb 954 xoranor 1355 19.33 1460 hbor 1525 nford 1546 19.30dc 1606 19.43 1607 19.32r 1658 euor2 2057 mooran2 2072 r19.32r 2578 undif3ss 3337 undif4 3425 issod 4241 onsucelsucexmid 4445 sucprcreg 4464 0elnn 4532 acexmidlemph 5767 nntri3or 6389 swoord1 6458 swoord2 6459 exmidaclem 7064 addlocprlem 7343 nqprloc 7353 apreap 8349 zletric 9098 zlelttric 9099 zmulcl 9107 zdceq 9126 zdcle 9127 zdclt 9128 nn0lt2 9132 elnn1uz2 9401 mnflt 9569 mnfltpnf 9571 xrltso 9582 fzdcel 9820 fzm1 9880 qletric 10021 qlelttric 10022 qdceq 10024 nn0o1gt2 11602 bj-fadc 12960 decidin 13004 triap 13224 |
Copyright terms: Public domain | W3C validator |