Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpjaod | Unicode version |
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
jaod.1 | |
jaod.2 | |
jaod.3 |
Ref | Expression |
---|---|
mpjaod |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaod.3 | . 2 | |
2 | jaod.1 | . . 3 | |
3 | jaod.2 | . . 3 | |
4 | 2, 3 | jaod 691 | . 2 |
5 | 1, 4 | mpd 13 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: ifbothdc 3474 opth1 4128 onsucelsucexmidlem 4414 reldmtpos 6118 dftpos4 6128 nnm00 6393 xpfi 6786 omp1eomlem 6947 ctmlemr 6961 ctssdclemn0 6963 finomni 6980 indpi 7118 enq0tr 7210 prarloclem3step 7272 distrlem4prl 7360 distrlem4pru 7361 lelttr 7820 nn1suc 8707 nnsub 8727 nn0lt2 9100 uzin 9326 xrlelttr 9557 xlesubadd 9634 fzfig 10171 seq3id 10249 seq3z 10252 faclbnd 10455 facavg 10460 bcval5 10477 hashfzo 10536 iserex 11076 fsum3cvg 11114 fsumf1o 11127 fisumss 11129 fsumcl2lem 11135 fsumadd 11143 fsummulc2 11185 isumsplit 11228 absdvdsb 11438 dvdsabsb 11439 dvdsabseq 11472 m1exp1 11525 flodddiv4 11558 gcdaddm 11599 gcdabs1 11604 lcmdvds 11687 prmind2 11728 rpexp 11758 trilpolemcl 13157 trilpolemlt1 13161 |
Copyright terms: Public domain | W3C validator |