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 700 | . . 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 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: oibabs 704 pm1.4 717 olci 722 pm2.07 727 pm2.46 729 biorf 734 pm1.5 755 pm2.41 766 pm4.78i 772 pm3.48 775 ordi 806 andi 808 pm4.72 813 stdcn 833 pm2.54dc 877 pm2.85dc 891 dcor 920 dedlemb 955 xoranor 1359 19.33 1464 hbor 1526 nford 1547 19.30dc 1607 19.43 1608 19.32r 1660 euor2 2064 mooran2 2079 r19.32r 2603 undif3ss 3368 undif4 3456 issod 4279 onsucelsucexmid 4489 sucprcreg 4508 0elnn 4578 acexmidlemph 5817 nntri3or 6440 swoord1 6509 swoord2 6510 exmidaclem 7143 exmidontri2or 7178 addlocprlem 7455 nqprloc 7465 apreap 8462 zletric 9211 zlelttric 9212 zmulcl 9220 zdceq 9239 zdcle 9240 zdclt 9241 nn0lt2 9245 elnn1uz2 9518 mnflt 9690 mnfltpnf 9692 xrltso 9703 fzdcel 9942 fzm1 10002 qletric 10143 qlelttric 10144 qdceq 10146 nn0o1gt2 11796 bj-fadc 13337 decidin 13382 triap 13611 tridceq 13638 |
Copyright terms: Public domain | W3C validator |