![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > olcd | GIF version |
Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Ref | Expression |
---|---|
orcd.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
olcd | ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcd.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | orcd 723 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
3 | 2 | orcomd 719 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.48 731 pm2.49 732 orim12i 749 pm1.5 755 dcan 919 dcor 920 dcun 3478 exmidn0m 4132 regexmidlem1 4456 reg2exmidlema 4457 nn0suc 4526 nndceq0 4539 acexmidlem1 5778 nntri3or 6397 nntri2or2 6402 nndceq 6403 nndcel 6404 nnm00 6433 ssfilem 6777 diffitest 6789 tridc 6801 finexdc 6804 fientri3 6811 unsnfidcex 6816 unsnfidcel 6817 fidcenumlemrks 6849 fidcenumlemrk 6850 finomni 7020 exmidfodomrlemeldju 7072 exmidfodomrlemreseldju 7073 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 exmidaclem 7081 mullocprlem 7402 recexprlemloc 7463 gt0ap0 8412 ltap 8419 recexaplem2 8437 nn1m1nn 8762 nn1gt1 8778 ltpnf 9597 mnflt 9599 xrltso 9612 xrpnfdc 9655 xrmnfdc 9656 exfzdc 10048 apbtwnz 10078 expnnval 10327 exp0 10328 bc0k 10534 bcpasc 10544 xrmaxadd 11062 sumdc 11159 zsumdc 11185 fsum3 11188 fisumss 11193 isumss2 11194 fsumsplit 11208 zproddc 11380 fprodseq 11384 infssuzex 11678 ctiunctlemudc 11986 suplociccreex 12810 djurclALT 13180 bj-nn0suc0 13319 trilpolemres 13410 trirec0 13412 |
Copyright terms: Public domain | W3C validator |