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 774 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | |
4 | 1, 2, 3 | syl2anc 408 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 697 |
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 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orim1d 776 orim2d 777 3orim123d 1298 19.33b2 1608 eqifdc 3501 preq12b 3692 prel12 3693 exmidsssnc 4121 funun 5162 nnsucelsuc 6380 nnaord 6398 nnmord 6406 swoer 6450 fidceq 6756 fin0or 6773 enomnilem 7003 exmidomni 7007 fodjuomnilemres 7013 ltsopr 7397 cauappcvgprlemloc 7453 caucvgprlemloc 7476 caucvgprprlemloc 7504 suplocexprlemloc 7522 mulextsr1lem 7581 suplocsrlemb 7607 axpre-suploclemres 7702 reapcotr 8353 apcotr 8362 mulext1 8367 mulext 8369 mul0eqap 8424 peano2z 9083 zeo 9149 uzm1 9349 eluzdc 9397 fzospliti 9946 frec2uzltd 10169 absext 10828 qabsor 10840 maxleast 10978 dvdslelemd 11530 odd2np1lem 11558 odd2np1 11559 isprm6 11814 ennnfonelemrnh 11918 dedekindeulemloc 12755 suplociccreex 12760 dedekindicclemloc 12764 ivthinclemloc 12777 uzdcinzz 12994 bj-findis 13166 nninfomnilem 13203 isomninnlem 13214 |
Copyright terms: Public domain | W3C validator |