![]() |
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 861 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 846 |
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 847 |
This theorem is referenced by: truorfal 1580 prid1g 4762 isso2i 5621 mpo0v 7487 0wdom 9560 nneo 12641 mnfltpnf 13101 bcpasc 14276 isumless 15786 binomfallfaclem2 15979 lcmfunsnlem2lem1 16570 srabaseOLD 20780 sraaddgOLD 20782 sramulrOLD 20784 m2detleib 22114 fctop 22488 cctop 22490 ovoliunnul 25005 vitalilem5 25110 logtayl 26149 bpos1 26765 0slt1s 27309 usgrexmpldifpr 28494 cffldtocusgr 28683 pthdlem2 29004 inindif 31731 disjunsn 31802 circlemethhgt 33592 fmla0disjsuc 34326 disjressuc2 37195 ifpimimb 42187 ifpimim 42192 binomcxplemnn0 43040 binomcxplemnotnn0 43047 salexct 44984 onenotinotbothi 45577 twonotinotbothi 45578 clifte 45579 cliftet 45580 paireqne 46113 sbgoldbo 46389 zlmodzxzldeplem 47080 ldepslinc 47091 line2x 47341 inlinecirc02plem 47373 alimp-surprise 47728 aacllem 47749 |
Copyright terms: Public domain | W3C validator |