![]() |
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 861 | 1 ⊢ (𝜓 ∨ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ 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: falortru 1581 opthhausdorff 5479 sucidg 6403 kmlem2 10094 sornom 10220 leid 11258 pnf0xnn0 12499 xrleid 13077 xmul01 13193 bcn1 14220 odd2np1lem 16229 lcm0val 16477 lcmfunsnlem2lem1 16521 lcmfunsnlem2 16523 coprmprod 16544 coprmproddvdslem 16545 prmrec 16801 smndex2dnrinv 18732 sratsetOLD 20668 sradsOLD 20671 m2detleib 21996 zclmncvs 24528 itg0 25160 itgz 25161 coemullem 25627 ftalem5 26442 chp1 26532 prmorcht 26543 pclogsum 26579 logexprlim 26589 bpos1 26647 addsqnreup 26807 pntpbnd1 26950 axlowdimlem16 27948 usgrexmpldifpr 28248 cusgrsizeindb1 28440 pthdlem2 28758 ex-or 29407 plymulx0 33199 signstfvn 33221 bj-0eltag 35478 bj-inftyexpidisj 35710 mblfinlem2 36145 volsupnfl 36152 12gcd5e1 40489 ifpdfor 41811 ifpim1 41815 ifpnot 41816 ifpid2 41817 ifpim2 41818 ifpim1g 41847 ifpbi1b 41849 icccncfext 44202 fourierdlem103 44524 fourierdlem104 44525 etransclem24 44573 etransclem35 44584 abnotataxb 45225 dandysum2p2e4 45307 paireqne 45777 sbgoldbo 46053 zlmodzxzldeplem 46653 line2x 46914 aacllem 47322 |
Copyright terms: Public domain | W3C validator |