![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > olci | 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 |
---|---|
olci | ⊢ (𝜓 ∨ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orci.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | a1i 11 | . 2 ⊢ (¬ 𝜓 → 𝜑) |
3 | 2 | orri 851 | 1 ⊢ (𝜓 ∨ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 836 |
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 199 df-or 837 |
This theorem is referenced by: falortru 1641 opthhausdorff 5214 sucidg 6054 kmlem2 9308 sornom 9434 leid 10472 pnf0xnn0 11721 xrleid 12294 xmul01 12409 bcn1 13418 odd2np1lem 15468 lcm0val 15713 lcmfunsnlem2lem1 15757 lcmfunsnlem2 15759 coprmprod 15780 coprmproddvdslem 15781 prmrec 16030 sratset 19581 srads 19583 m2detleib 20842 zclmncvs 23355 itg0 23983 itgz 23984 coemullem 24443 ftalem5 25255 chp1 25345 prmorcht 25356 pclogsum 25392 logexprlim 25402 bpos1 25460 pntpbnd1 25727 axlowdimlem16 26306 usgrexmpldifpr 26605 cusgrsizeindb1 26798 pthdlem2 27120 ex-or 27853 plymulx0 31224 bj-0eltag 33538 bj-inftyexpidisj 33687 mblfinlem2 34073 volsupnfl 34080 ifpdfor 38767 ifpim1 38771 ifpnot 38772 ifpid2 38773 ifpim2 38774 ifpim1g 38804 ifpbi1b 38806 icccncfext 41028 fourierdlem103 41353 fourierdlem104 41354 etransclem24 41402 etransclem35 41413 abnotataxb 42010 dandysum2p2e4 42092 paireqne 42450 sbgoldbo 42700 zlmodzxzldeplem 43302 line2x 43490 aacllem 43653 |
Copyright terms: Public domain | W3C validator |