Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orcd | GIF version |
Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.) |
Ref | Expression |
---|---|
orcd.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
orcd | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | orc 686 | . 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-io 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: olcd 708 pm2.47 714 orim12i 733 dcor 904 undif3ss 3307 dcun 3443 exmidn0m 4094 exmidsssn 4095 reg2exmidlema 4419 acexmidlem1 5738 poxp 6097 nntri2or2 6362 nnm00 6393 ssfilem 6737 diffitest 6749 tridc 6761 finexdc 6764 fientri3 6771 unsnfidcex 6776 unsnfidcel 6777 fidcenumlemrks 6809 finomni 6980 exmidfodomrlemeldju 7023 exmidfodomrlemreseldju 7024 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 exmidaclem 7032 nqprloc 7321 mullocprlem 7346 recexprlemloc 7407 ltxrlt 7798 zmulcl 9075 nn0lt2 9100 zeo 9124 xrltso 9550 apbtwnz 10015 expnegap0 10269 xrmaxadd 10998 zsumdc 11121 fsumsplit 11144 sumsplitdc 11169 isumlessdc 11233 suplociccreex 12698 djulclALT 12935 trilpolemres 13162 |
Copyright terms: Public domain | W3C validator |