![]() |
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 114 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 114 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 2, 4 | jaod 689 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
6 | 5 | imp 123 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∨ wo 680 |
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 681 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpjaodan 770 ordi 788 andi 790 dcor 902 ccase 931 mpjao3dan 1268 relop 4649 poltletr 4897 tfrlemisucaccv 6176 tfr1onlemsucaccv 6192 tfrcllemsucaccv 6205 phplem3 6701 ssfilem 6722 diffitest 6734 reapmul1 8275 apsqgt0 8281 recexaplem2 8326 nnnn0addcl 8911 un0addcl 8914 un0mulcl 8915 elz2 9026 xrltso 9475 xaddnemnf 9533 xaddnepnf 9534 fzsplit2 9723 fzsuc2 9752 elfzp12 9772 expp1 10193 expnegap0 10194 expcllem 10197 mulexpzap 10226 expaddzap 10230 expmulzap 10232 bcpasc 10405 xrltmaxsup 10918 xrmaxaddlem 10921 summodc 11044 fsumsplit 11068 ef0lem 11217 odd2np1 11418 dvdslcm 11596 lcmeq0 11598 lcmcl 11599 lcmneg 11601 lcmgcd 11605 rpexp1i 11678 |
Copyright terms: Public domain | W3C validator |