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 712 | . 2 |
6 | 5 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 703 |
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 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpjaodan 793 ordi 811 andi 813 dcor 930 ccase 959 mpjao3dan 1302 relop 4759 poltletr 5009 tfrlemisucaccv 6301 tfr1onlemsucaccv 6317 tfrcllemsucaccv 6330 phplem3 6828 ssfilem 6849 diffitest 6861 reapmul1 8501 apsqgt0 8507 recexaplem2 8557 nnnn0addcl 9152 un0addcl 9155 un0mulcl 9156 elz2 9270 xrltso 9740 xaddnemnf 9801 xaddnepnf 9802 fzsplit2 9993 fzsuc2 10022 elfzp12 10042 expp1 10470 expnegap0 10471 expcllem 10474 mulexpzap 10503 expaddzap 10507 expmulzap 10509 bcpasc 10687 xrltmaxsup 11207 xrmaxaddlem 11210 summodc 11333 fsumsplit 11357 fprodsplitdc 11546 ef0lem 11610 odd2np1 11819 dvdslcm 12010 lcmeq0 12012 lcmcl 12013 lcmneg 12015 lcmgcd 12019 rpexp1i 12095 pcid 12264 lgsdir2lem4 13647 lgsdir2 13649 lgsdirnn0 13663 lgsdinn0 13664 |
Copyright terms: Public domain | W3C validator |