| 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 718 |
. 2
|
| 5 | 1, 4 | mpd 13 |
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 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: ifbothdc 3604 opth1 4279 onsucelsucexmidlem 4576 reldmtpos 6338 dftpos4 6348 nnm00 6615 xpfi 7028 omp1eomlem 7195 ctmlemr 7209 ctssdclemn0 7211 finomni 7241 indpi 7454 enq0tr 7546 prarloclem3step 7608 distrlem4prl 7696 distrlem4pru 7697 lelttr 8160 nn1suc 9054 nnsub 9074 nn0lt2 9453 uzin 9680 xrlelttr 9927 xlesubadd 10004 fzfig 10573 seq3id 10668 seq3z 10671 faclbnd 10884 facavg 10889 bcval5 10906 hashfzo 10965 iserex 11621 fsum3cvg 11660 fsumf1o 11672 fisumss 11674 fsumcl2lem 11680 fsumadd 11688 fsummulc2 11730 isumsplit 11773 fprodf1o 11870 prodssdc 11871 fprodssdc 11872 fprodmul 11873 absdvdsb 12091 dvdsabsb 12092 dvdsabseq 12129 m1exp1 12183 flodddiv4 12218 gcdaddm 12276 gcdabs1 12281 lcmdvds 12372 prmind2 12413 rpexp 12446 fermltl 12527 pcxnn0cl 12604 pcxcl 12605 pcabs 12620 pcmpt 12637 pockthg 12651 mulgnn0ass 13465 lgseisenlem2 15519 2lgslem1c 15538 trilpolemcl 15938 trilpolemlt1 15942 |
| Copyright terms: Public domain | W3C validator |