![]() |
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 735 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | |
4 | 1, 2, 3 | syl2anc 404 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 665 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orim1d 737 orim2d 738 3orim123d 1257 19.33b2 1566 eqifdc 3429 preq12b 3620 prel12 3621 funun 5071 nnsucelsuc 6266 nnaord 6282 nnmord 6290 swoer 6334 fidceq 6639 fin0or 6656 enomnilem 6855 exmidomni 6859 fodjuomnilemres 6864 ltsopr 7216 cauappcvgprlemloc 7272 caucvgprlemloc 7295 caucvgprprlemloc 7323 mulextsr1lem 7386 reapcotr 8136 apcotr 8145 mulext1 8150 mulext 8152 peano2z 8847 zeo 8912 uzm1 9110 eluzdc 9158 fzospliti 9648 frec2uzltd 9871 absext 10557 qabsor 10569 maxleast 10707 dvdslelemd 11183 odd2np1lem 11211 odd2np1 11212 isprm6 11465 uzdcinzz 11971 bj-findis 12147 nninfomnilem 12182 |
Copyright terms: Public domain | W3C validator |