| 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 11592 fsum3cvg 11631 fsumf1o 11643 fisumss 11645 fsumcl2lem 11651 fsumadd 11659 fsummulc2 11701 isumsplit 11744 fprodf1o 11841 prodssdc 11842 fprodssdc 11843 fprodmul 11844 absdvdsb 12062 dvdsabsb 12063 dvdsabseq 12100 m1exp1 12154 flodddiv4 12189 gcdaddm 12247 gcdabs1 12252 lcmdvds 12343 prmind2 12384 rpexp 12417 fermltl 12498 pcxnn0cl 12575 pcxcl 12576 pcabs 12591 pcmpt 12608 pockthg 12622 mulgnn0ass 13436 lgseisenlem2 15490 2lgslem1c 15509 trilpolemcl 15909 trilpolemlt1 15913 |
| Copyright terms: Public domain | W3C validator |