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 8703 nnsub 8723 nn0lt2 9090 uzin 9314 xrlelttr 9544 xlesubadd 9621 fzfig 10158 seq3id 10236 seq3z 10239 faclbnd 10442 facavg 10447 bcval5 10464 hashfzo 10523 iserex 11063 fsum3cvg 11101 fsumf1o 11114 fisumss 11116 fsumcl2lem 11122 fsumadd 11130 fsummulc2 11172 isumsplit 11215 absdvdsb 11423 dvdsabsb 11424 dvdsabseq 11457 m1exp1 11510 flodddiv4 11543 gcdaddm 11584 gcdabs1 11589 lcmdvds 11672 prmind2 11713 rpexp 11743 trilpolemcl 13126 trilpolemlt1 13130 |
Copyright terms: Public domain | W3C validator |