![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orci | GIF version |
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
orci.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
orci | ⊢ (𝜑 ∨ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orci.1 | . 2 ⊢ 𝜑 | |
2 | orc 712 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ∨ wo 708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: truorfal 1406 prid1g 3695 onsucelsucexmidlem1 4524 regexmidlemm 4528 nn0suc 4600 nndceq0 4614 0elnn 4615 acexmidlem2 5866 dcfi 6974 exmidaclem 7201 indpi 7329 sup3exmid 8900 nn1gt1 8939 nneoor 9341 mnfltpnf 9769 bcpasc 10727 dceqnconst 14456 nconstwlpolem0 14459 |
Copyright terms: Public domain | W3C validator |