![]() |
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 3582 opth1 4254 onsucelsucexmidlem 4546 reldmtpos 6277 dftpos4 6287 nnm00 6554 xpfi 6957 omp1eomlem 7122 ctmlemr 7136 ctssdclemn0 7138 finomni 7167 indpi 7370 enq0tr 7462 prarloclem3step 7524 distrlem4prl 7612 distrlem4pru 7613 lelttr 8075 nn1suc 8967 nnsub 8987 nn0lt2 9363 uzin 9589 xrlelttr 9835 xlesubadd 9912 fzfig 10460 seq3id 10538 seq3z 10541 faclbnd 10752 facavg 10757 bcval5 10774 hashfzo 10833 iserex 11378 fsum3cvg 11417 fsumf1o 11429 fisumss 11431 fsumcl2lem 11437 fsumadd 11445 fsummulc2 11487 isumsplit 11530 fprodf1o 11627 prodssdc 11628 fprodssdc 11629 fprodmul 11630 absdvdsb 11847 dvdsabsb 11848 dvdsabseq 11884 m1exp1 11937 flodddiv4 11970 gcdaddm 12016 gcdabs1 12021 lcmdvds 12110 prmind2 12151 rpexp 12184 fermltl 12265 pcxnn0cl 12341 pcxcl 12342 pcabs 12357 pcmpt 12374 pockthg 12388 mulgnn0ass 13095 lgseisenlem2 14904 trilpolemcl 15239 trilpolemlt1 15243 |
Copyright terms: Public domain | W3C validator |