![]() |
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 115 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 115 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 2, 4 | jaod 718 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
6 | 5 | imp 124 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mpjaodan 799 ordi 817 andi 819 dcor 937 ccase 966 mpjao3dan 1318 relop 4795 poltletr 5047 tfrlemisucaccv 6349 tfr1onlemsucaccv 6365 tfrcllemsucaccv 6378 phplem3 6881 ssfilem 6902 diffitest 6914 reapmul1 8581 apsqgt0 8587 recexaplem2 8638 nnnn0addcl 9235 un0addcl 9238 un0mulcl 9239 elz2 9353 xrltso 9825 xaddnemnf 9886 xaddnepnf 9887 fzsplit2 10079 fzsuc2 10108 elfzp12 10128 expp1 10557 expnegap0 10558 expcllem 10561 mulexpzap 10590 expaddzap 10594 expmulzap 10596 zzlesq 10719 bcpasc 10777 xrltmaxsup 11296 xrmaxaddlem 11299 summodc 11422 fsumsplit 11446 fprodsplitdc 11635 ef0lem 11699 odd2np1 11909 dvdslcm 12100 lcmeq0 12102 lcmcl 12103 lcmneg 12105 lcmgcd 12109 rpexp1i 12185 pcid 12355 4sqlem16 12437 xpsfeq 12818 mulgneg 13077 mulgnn0z 13086 lgsdir2lem4 14885 lgsdir2 14887 lgsdirnn0 14901 lgsdinn0 14902 |
Copyright terms: Public domain | W3C validator |