Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jaodan | Unicode 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 691 | . 2 |
6 | 5 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 682 |
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 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpjaodan 772 ordi 790 andi 792 dcor 904 ccase 933 mpjao3dan 1270 relop 4659 poltletr 4909 tfrlemisucaccv 6190 tfr1onlemsucaccv 6206 tfrcllemsucaccv 6219 phplem3 6716 ssfilem 6737 diffitest 6749 reapmul1 8325 apsqgt0 8331 recexaplem2 8381 nnnn0addcl 8975 un0addcl 8978 un0mulcl 8979 elz2 9090 xrltso 9550 xaddnemnf 9608 xaddnepnf 9609 fzsplit2 9798 fzsuc2 9827 elfzp12 9847 expp1 10268 expnegap0 10269 expcllem 10272 mulexpzap 10301 expaddzap 10305 expmulzap 10307 bcpasc 10480 xrltmaxsup 10994 xrmaxaddlem 10997 summodc 11120 fsumsplit 11144 ef0lem 11293 odd2np1 11497 dvdslcm 11677 lcmeq0 11679 lcmcl 11680 lcmneg 11682 lcmgcd 11686 rpexp1i 11759 |
Copyright terms: Public domain | W3C validator |