Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jaod | GIF version |
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.) |
Ref | Expression |
---|---|
jaod.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jaod.2 | ⊢ (𝜑 → (𝜃 → 𝜒)) |
Ref | Expression |
---|---|
jaod | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaod.1 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | com12 27 | . . 3 ⊢ (𝜓 → (𝜑 → 𝜒)) |
3 | jaod.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜒)) | |
4 | 3 | com12 27 | . . 3 ⊢ (𝜃 → (𝜑 → 𝜒)) |
5 | 2, 4 | jaoi 636 | . 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒)) |
6 | 5 | com12 27 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: mpjaod 638 jaao 639 orel2 645 pm2.621 666 mtord 697 jaodan 710 pm2.63 713 pm2.74 720 dedlema 876 dedlemb 877 oplem1 882 opthpr 3543 trsucss 4160 ordsucim 4226 onsucelsucr 4234 0elnn 4340 xpsspw 4450 relop 4486 fununi 4967 poxp 5853 nntri1 6074 nnsseleq 6079 nnmordi 6089 nnaordex 6100 nnm00 6102 swoord2 6136 nneneq 6320 elni2 6412 prubl 6584 distrlem4prl 6682 distrlem4pru 6683 ltxrlt 7085 recexre 7569 remulext1 7590 mulext1 7603 un0addcl 8215 un0mulcl 8216 elnnz 8255 zleloe 8292 zindd 8356 uzsplit 8954 fzm1 8962 expcl2lemap 9267 expnegzap 9289 expaddzap 9299 expmulzap 9301 recvguniq 9593 absexpzap 9676 bj-nntrans 10076 bj-nnelirr 10078 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |