![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orc | GIF version |
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
orc | ⊢ (φ → (φ ∨ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ ((φ ∨ ψ) → (φ ∨ ψ)) | |
2 | jaob 630 | . . 3 ⊢ (((φ ∨ ψ) → (φ ∨ ψ)) ↔ ((φ → (φ ∨ ψ)) ∧ (ψ → (φ ∨ ψ)))) | |
3 | 1, 2 | mpbi 133 | . 2 ⊢ ((φ → (φ ∨ ψ)) ∧ (ψ → (φ ∨ ψ))) |
4 | 3 | simpli 104 | 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-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm2.67-2 633 pm1.4 645 orci 649 orcd 651 orcs 653 pm2.45 656 biorfi 664 pm1.5 681 pm2.4 694 pm4.44 695 pm4.45 697 pm3.48 698 pm2.76 720 orabs 726 ordi 728 andi 730 pm4.72 735 biort 737 dcim 783 pm2.54dc 789 pm4.78i 807 pm2.85dc 810 dcor 842 pm5.71dc 867 dedlema 875 3mix1 1072 xoranor 1267 19.33 1370 hbor 1435 nford 1456 19.30dc 1515 19.43 1516 19.32r 1567 moor 1968 r19.32r 2451 ssun1 3100 undif3ss 3192 reuun1 3213 prmg 3480 opthpr 3534 issod 4047 elelsuc 4112 regexmidlem1 4218 nndceq 6015 nndcel 6016 swoord1 6071 swoord2 6072 addlocprlem 6518 msqge0 7400 mulge0 7403 ltleap 7413 nn1m1nn 7713 elnnz 8031 zletric 8065 zlelttric 8066 zmulcl 8073 zdceq 8092 zdcle 8093 zdclt 8094 ltpnf 8472 xrlttri3 8488 fzdcel 8674 bj-nn0suc0 9410 |
Copyright terms: Public domain | W3C validator |