![]() |
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 707 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | imp 123 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpjaodan 788 ordi 806 andi 808 dcor 920 ccase 949 mpjao3dan 1286 relop 4729 poltletr 4979 tfrlemisucaccv 6262 tfr1onlemsucaccv 6278 tfrcllemsucaccv 6291 phplem3 6788 ssfilem 6809 diffitest 6821 reapmul1 8449 apsqgt0 8455 recexaplem2 8505 nnnn0addcl 9099 un0addcl 9102 un0mulcl 9103 elz2 9214 xrltso 9681 xaddnemnf 9739 xaddnepnf 9740 fzsplit2 9930 fzsuc2 9959 elfzp12 9979 expp1 10404 expnegap0 10405 expcllem 10408 mulexpzap 10437 expaddzap 10441 expmulzap 10443 bcpasc 10617 xrltmaxsup 11131 xrmaxaddlem 11134 summodc 11257 fsumsplit 11281 fprodsplitdc 11470 ef0lem 11534 odd2np1 11737 dvdslcm 11917 lcmeq0 11919 lcmcl 11920 lcmneg 11922 lcmgcd 11926 rpexp1i 11999 |
Copyright terms: Public domain | W3C validator |