![]() |
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 702 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: truorfal 1385 prid1g 3659 onsucelsucexmidlem1 4481 regexmidlemm 4485 nn0suc 4557 nndceq0 4571 0elnn 4572 acexmidlem2 5811 exmidaclem 7122 indpi 7241 sup3exmid 8807 nn1gt1 8846 nneoor 9245 mnfltpnf 9670 bcpasc 10617 dceqnconst 13571 nconstwlpolem0 13574 |
Copyright terms: Public domain | W3C validator |