![]() |
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 860 | 1 ⊢ (𝜓 ∨ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 845 |
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 846 |
This theorem is referenced by: falortru 1572 opthhausdorff 5519 sucidg 6452 kmlem2 10176 sornom 10302 leid 11342 pnf0xnn0 12584 xrleid 13165 xmul01 13281 bcn1 14308 odd2np1lem 16320 lcm0val 16568 lcmfunsnlem2lem1 16612 lcmfunsnlem2 16614 coprmprod 16635 coprmproddvdslem 16636 prmrec 16894 smndex2dnrinv 18875 sratsetOLD 21087 sradsOLD 21090 m2detleib 22577 zclmncvs 25120 itg0 25753 itgz 25754 coemullem 26229 ftalem5 27054 chp1 27144 prmorcht 27155 pclogsum 27193 logexprlim 27203 bpos1 27261 addsqnreup 27421 pntpbnd1 27564 axlowdimlem16 28840 usgrexmpldifpr 29143 cusgrsizeindb1 29336 pthdlem2 29654 ex-or 30303 plymulx0 34310 signstfvn 34332 bj-0eltag 36588 bj-inftyexpidisj 36820 mblfinlem2 37262 volsupnfl 37269 12gcd5e1 41606 ifpdfor 43037 ifpim1 43041 ifpnot 43042 ifpid2 43043 ifpim2 43044 ifpim1g 43073 ifpbi1b 43075 icccncfext 45413 fourierdlem103 45735 fourierdlem104 45736 etransclem24 45784 etransclem35 45795 abnotataxb 46436 dandysum2p2e4 46518 paireqne 46988 sbgoldbo 47264 zlmodzxzldeplem 47752 line2x 48013 aacllem 48420 |
Copyright terms: Public domain | W3C validator |