![]() |
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 630 | . . 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 628 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm1.4 645 olci 650 pm2.07 655 pm2.46 657 biorf 662 pm1.5 681 pm2.41 692 pm3.48 698 ordi 728 andi 730 pm4.72 735 pm2.54dc 789 oibabs 799 pm4.78i 807 pm2.85dc 810 dcor 842 dedlemb 876 xoranor 1267 19.33 1370 hbor 1435 nford 1456 19.30dc 1515 19.43 1516 19.32r 1567 euor2 1955 mooran2 1970 r19.32r 2451 undif3ss 3192 undif4 3278 issod 4047 onsucelsucexmid 4215 sucprcreg 4227 0elnn 4283 acexmidlemph 5448 nntri3or 6011 swoord1 6071 swoord2 6072 addlocprlem 6518 nqprloc 6528 apreap 7371 zletric 8065 zlelttric 8066 zmulcl 8073 zdceq 8092 zdcle 8093 zdclt 8094 nn0lt2 8098 elnn1uz2 8320 mnflt 8474 mnfltpnf 8476 xrltso 8487 fzdcel 8674 fzm1 8732 |
Copyright terms: Public domain | W3C validator |