Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orci | Structured version Visualization version GIF version |
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Ref | Expression |
---|---|
orci.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
orci | ⊢ (𝜑 ∨ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orci.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | pm2.24i 145 | . 2 ⊢ (¬ 𝜑 → 𝜓) |
3 | 2 | orri 390 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 382 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-or 384 |
This theorem is referenced by: truorfal 1502 prid1g 4239 isso2i 4991 0wdom 8358 nneo 11337 mnfltpnf 11836 bcpasc 12970 isumless 14416 binomfallfaclem2 14610 lcmfunsnlem2lem1 15189 srabase 18999 sraaddg 19000 sramulr 19001 m2detleib 20256 fctop 20618 cctop 20620 ovoliunnul 23082 vitalilem5 23187 logtayl 24206 bpos1 24808 usgraexmpldifpr 25928 inindif 28738 disjunsn 28789 ifpimimb 36868 ifpimim 36873 binomcxplemnn0 37570 binomcxplemnotnn0 37577 salexct 39228 onenotinotbothi 39749 twonotinotbothi 39750 clifte 39751 cliftet 39752 pthdlem2 40974 zlmodzxzldeplem 42081 ldepslinc 42092 alimp-surprise 42335 aacllem 42356 |
Copyright terms: Public domain | W3C validator |