![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jaodan | GIF version |
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
jaodan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
jaodan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
Ref | Expression |
---|---|
jaodan | ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaodan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 113 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 113 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 2, 4 | jaod 670 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
6 | 5 | imp 122 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∨ wo 662 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: mpjaodan 745 ordi 763 andi 765 dcor 877 ccase 906 mpjao3dan 1239 relop 4514 poltletr 4755 tfrlemisucaccv 5974 tfr1onlemsucaccv 5990 tfrcllemsucaccv 6003 phplem3 6389 ssfilem 6410 diffitest 6421 reapmul1 7762 apsqgt0 7768 recexaplem2 7809 nnnn0addcl 8385 un0addcl 8388 un0mulcl 8389 elz2 8500 xrltso 8947 fzsplit2 9145 fzsuc2 9172 elfzp12 9192 expp1 9580 expnegap0 9581 expcllem 9584 mulexpzap 9613 expaddzap 9617 expmulzap 9619 bcpasc 9790 odd2np1 10417 dvdslcm 10595 lcmeq0 10597 lcmcl 10598 lcmneg 10600 lcmgcd 10604 rpexp1i 10677 |
Copyright terms: Public domain | W3C validator |