![]() |
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 689 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpd 13 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ifbothdc 3468 opth1 4116 onsucelsucexmidlem 4402 reldmtpos 6102 dftpos4 6112 nnm00 6377 xpfi 6769 omp1eomlem 6929 ctmlemr 6943 ctssdclemn0 6945 finomni 6960 indpi 7092 enq0tr 7184 prarloclem3step 7246 distrlem4prl 7334 distrlem4pru 7335 lelttr 7769 nn1suc 8643 nnsub 8663 nn0lt2 9030 uzin 9254 xrlelttr 9476 xlesubadd 9553 fzfig 10090 seq3id 10168 seq3z 10171 faclbnd 10374 facavg 10379 bcval5 10396 hashfzo 10455 iserex 10994 fsum3cvg 11032 fsumf1o 11045 fisumss 11047 fsumcl2lem 11053 fsumadd 11061 fsummulc2 11103 isumsplit 11146 absdvdsb 11353 dvdsabsb 11354 dvdsabseq 11387 m1exp1 11440 flodddiv4 11473 gcdaddm 11514 gcdabs1 11519 lcmdvds 11600 prmind2 11641 rpexp 11671 trilpolemcl 12911 trilpolemlt1 12915 |
Copyright terms: Public domain | W3C validator |