![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > olci | Structured version Visualization version Unicode 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 378 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: falortru 1472 sucidg 5501 kmlem2 8581 sornom 8707 leid 9729 xrleid 11449 xmul01 11553 bcn1 12498 odd2np1lem 14364 lcm0val 14558 lcmfunsnlem2lem1 14611 lcmfunsnlem2 14613 coprmprod 14678 coprmproddvdslem 14679 prmrec 14866 sratset 18407 srads 18409 m2detleib 19656 itg0 22737 itgz 22738 coemullem 23204 ftalem5 24001 ftalem5OLD 24003 chp1 24094 prmorcht 24105 pclogsum 24143 logexprlim 24153 bpos1 24211 pntpbnd1 24424 axlowdimlem16 24987 usgraexmpldifpr 25127 cusgrasizeindb1 25199 vdgrf 25626 ex-or 25871 plymulx0 29436 bj-0eltag 31572 bj-inftyexpidisj 31652 mblfinlem2 31978 volsupnfl 31985 ifpdfor 36108 ifpim1 36112 ifpnot 36113 ifpid2 36114 ifpim2 36115 ifpim1g 36145 ifpbi1b 36147 icccncfext 37765 fourierdlem103 38073 fourierdlem104 38074 etransclem24 38123 etransclem35 38134 abnotataxb 38504 dandysum2p2e4 38586 pnf0xnn0 39078 cusgrsizeindb1 39511 zlmodzxzldeplem 40344 aacllem 40593 |
Copyright terms: Public domain | W3C validator |