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 153 | . 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 210 df-or 847 |
This theorem is referenced by: truorfal 1580 trunortruOLD 1592 trunorfalOLD 1594 prid1g 4651 isso2i 5477 mpo0v 7252 0wdom 9107 nneo 12147 mnfltpnf 12604 bcpasc 13773 isumless 15293 binomfallfaclem2 15486 lcmfunsnlem2lem1 16079 srabase 20069 sraaddg 20070 sramulr 20071 m2detleib 21382 fctop 21755 cctop 21757 ovoliunnul 24259 vitalilem5 24364 logtayl 25403 bpos1 26019 usgrexmpldifpr 27200 cffldtocusgr 27389 pthdlem2 27709 inindif 30437 disjunsn 30507 circlemethhgt 32193 fmla0disjsuc 32931 0slt1s 33664 ifpimimb 40665 ifpimim 40670 binomcxplemnn0 41505 binomcxplemnotnn0 41512 salexct 43415 onenotinotbothi 43967 twonotinotbothi 43968 clifte 43969 cliftet 43970 paireqne 44497 sbgoldbo 44773 zlmodzxzldeplem 45373 ldepslinc 45384 line2x 45634 inlinecirc02plem 45666 alimp-surprise 45937 aacllem 45958 |
Copyright terms: Public domain | W3C validator |