![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orim2d | GIF version |
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Ref | Expression |
---|---|
orim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
orim2d | ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 21 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
2 | orim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | orim12d 787 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orim2 790 orbi2d 791 pm2.82 813 stdcndcOLD 847 pm2.13dc 886 exmid1dc 4218 acexmidlemcase 5891 poxp 6257 fodjuomnilemdc 7172 omniwomnimkv 7195 exmidontriimlem1 7250 indpi 7371 suplocexprlemloc 7750 nneoor 9385 uzp1 9591 maxabslemlub 11248 xrmaxiflemlub 11288 exmidunben 12477 bj-nn0suc 15174 sbthomlem 15232 |
Copyright terms: Public domain | W3C validator |