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 391 | 1 ⊢ (𝜓 ∨ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 383 |
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 197 df-or 385 |
This theorem is referenced by: falortru 1512 sucidg 5803 kmlem2 8973 sornom 9099 leid 10133 pnf0xnn0 11370 xrleid 11983 xmul01 12097 bcn1 13100 odd2np1lem 15064 lcm0val 15307 lcmfunsnlem2lem1 15351 lcmfunsnlem2 15353 coprmprod 15375 coprmproddvdslem 15376 prmrec 15626 sratset 19184 srads 19186 m2detleib 20437 zclmncvs 22948 itg0 23546 itgz 23547 coemullem 24006 ftalem5 24803 chp1 24893 prmorcht 24904 pclogsum 24940 logexprlim 24950 bpos1 25008 pntpbnd1 25275 axlowdimlem16 25837 usgrexmpldifpr 26150 cusgrsizeindb1 26346 pthdlem2 26664 clwwlksn0 26907 ex-or 27278 plymulx0 30624 bj-0eltag 32966 bj-inftyexpidisj 33097 mblfinlem2 33447 volsupnfl 33454 ifpdfor 37809 ifpim1 37813 ifpnot 37814 ifpid2 37815 ifpim2 37816 ifpim1g 37846 ifpbi1b 37848 icccncfext 40100 fourierdlem103 40426 fourierdlem104 40427 etransclem24 40475 etransclem35 40486 abnotataxb 41083 dandysum2p2e4 41165 sbgoldbo 41675 zlmodzxzldeplem 42287 aacllem 42547 |
Copyright terms: Public domain | W3C validator |