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 150 | . 2 ⊢ (¬ 𝜑 → 𝜓) |
3 | 2 | orri 859 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 844 |
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 206 df-or 845 |
This theorem is referenced by: truorfal 1577 trunorfalOLD 1590 prid1g 4696 isso2i 5538 mpo0v 7359 0wdom 9329 nneo 12404 mnfltpnf 12862 bcpasc 14035 isumless 15557 binomfallfaclem2 15750 lcmfunsnlem2lem1 16343 srabaseOLD 20442 sraaddgOLD 20444 sramulrOLD 20446 m2detleib 21780 fctop 22154 cctop 22156 ovoliunnul 24671 vitalilem5 24776 logtayl 25815 bpos1 26431 usgrexmpldifpr 27625 cffldtocusgr 27814 pthdlem2 28136 inindif 30863 disjunsn 30933 circlemethhgt 32623 fmla0disjsuc 33360 0slt1s 34023 ifpimimb 41111 ifpimim 41116 binomcxplemnn0 41967 binomcxplemnotnn0 41974 salexct 43873 onenotinotbothi 44428 twonotinotbothi 44429 clifte 44430 cliftet 44431 paireqne 44963 sbgoldbo 45239 zlmodzxzldeplem 45839 ldepslinc 45850 line2x 46100 inlinecirc02plem 46132 alimp-surprise 46484 aacllem 46505 |
Copyright terms: Public domain | W3C validator |