olci - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > olci		Structured version Visualization version GIF version

Theorem olci 880

Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)

**Hypothesis**
Ref	Expression
orci.1	⊢ 𝜑

**Assertion**
Ref	Expression
olci	⊢ (𝜓 ∨ 𝜑)

**Proof of Theorem olci**
Step	Hyp	Ref	Expression
1		orci.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (¬ 𝜓 → 𝜑)
3	2	orri 876	1 ⊢ (𝜓 ∨ 𝜑)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ∨ wo 861

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This proof depends on definitions: df-bi 210 df-or 862

This theorem is used by: falortru 1608 opthhausdorff 5489 sucidg 6446 f1ounsn 7280 kmlem2 10230 sornom 10355 leid 11406 pnf0xnn0 12686 xrleid 13280 xmul01 13397 bcn1 14457 odd2np1lem 16510 lcm0val 16769 lcmfunsnlem2lem1 16813 lcmfunsnlem2 16815 coprmprod 16836 coprmproddvdslem 16837 prmrec 17100 smndex2dnrinv 19114 degenmgm 19137 degenmgm2 19140 m2detleib 22946 zclmncvs 25469 itg0 26100 itgz 26101 coemullem 26569 plyn0mulidp 26602 ftalem5 27404 chp1 27494 prmorcht 27505 pclogsum 27542 logexprlim 27552 bpos1 27610 addsqnreup 27770 pntpbnd1 27913 axlowdimlem16 29535 usgrexmpldifpr 29839 cusgrsizeindb1 30031 pthdlem2 30354 ex-or 31022 ply1coedeg 34121 signstfvn 35198 bj-0eltag 37891 bj-inftyexpidisj 38132 mblfinlem2 38577 volsupnfl 38584 12gcd5e1 43054 ifpdfor 44466 ifpim1 44470 ifpnot 44471 ifpid2 44472 ifpim2 44473 ifpim1g 44502 ifpbi1b 44504 icccncfext 46897 fourierdlem103 47219 fourierdlem104 47220 etransclem24 47268 etransclem35 47279 abnotataxb 47986 dandysum2p2e4 48068 paireqne 48593 sbgoldbo 48885 usgrexmpl1lem 49119 usgrexmpl1tri 49123 usgrexmpl2lem 49124 usgrexmpl2nb0 49129 usgrexmpl2nb2 49131 usgrexmpl2nb3 49132 usgrexmpl2nb4 49133 usgrexmpl2nb5 49134 gpgedg2iv 49165 gpg5nbgrvtx03starlem2 49167 gpg5nbgrvtx13starlem2 49170 gpgprismgr4cycllem2 49194 gpgprismgr4cycllem7 49199 gpg5edgnedg 49228 zlmodzxzldeplem 49610 line2x 49866 aacllem 50939