![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orim12d | GIF version |
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
Ref | Expression |
---|---|
orim12d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
orim12d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
orim12d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orim12d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | orim12d.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
3 | pm3.48 775 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | |
4 | 1, 2, 3 | syl2anc 409 | 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: orim1d 777 orim2d 778 3orim123d 1299 19.33b2 1609 eqifdc 3511 preq12b 3705 prel12 3706 exmidsssnc 4134 funun 5175 nnsucelsuc 6395 nnaord 6413 nnmord 6421 swoer 6465 fidceq 6771 fin0or 6788 enomnilem 7018 exmidomni 7022 fodjuomnilemres 7028 ltsopr 7428 cauappcvgprlemloc 7484 caucvgprlemloc 7507 caucvgprprlemloc 7535 suplocexprlemloc 7553 mulextsr1lem 7612 suplocsrlemb 7638 axpre-suploclemres 7733 reapcotr 8384 apcotr 8393 mulext1 8398 mulext 8400 mul0eqap 8455 peano2z 9114 zeo 9180 uzm1 9380 eluzdc 9431 fzospliti 9984 frec2uzltd 10207 absext 10867 qabsor 10879 maxleast 11017 dvdslelemd 11577 odd2np1lem 11605 odd2np1 11606 isprm6 11861 ennnfonelemrnh 11965 dedekindeulemloc 12805 suplociccreex 12810 dedekindicclemloc 12814 ivthinclemloc 12827 cos11 12982 uzdcinzz 13176 bj-findis 13348 nninfomnilem 13389 isomninnlem 13400 |
Copyright terms: Public domain | W3C validator |