![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpjao3dan | Unicode version |
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
Ref | Expression |
---|---|
mpjao3dan.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpjao3dan.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpjao3dan.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpjao3dan.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpjao3dan |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpjao3dan.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpjao3dan.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jaodan 797 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | mpjao3dan.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | mpjao3dan.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | df-3or 979 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | sylib 122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 4, 7 | mpjaodan 798 |
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 709 |
This theorem depends on definitions: df-bi 117 df-3or 979 |
This theorem is referenced by: wetriext 4576 nntri3 6497 nntri2or2 6498 nntr2 6503 tridc 6898 nnnninfeq 7125 exmidontriimlem2 7220 caucvgprlemnkj 7664 caucvgprlemnbj 7665 caucvgprprlemnkj 7690 caucvgprprlemnbj 7691 caucvgsr 7800 npnflt 9813 nmnfgt 9816 xleadd1a 9871 xltadd1 9874 xlt2add 9878 xsubge0 9879 xleaddadd 9885 addmodlteq 10395 iseqf1olemkle 10481 hashfiv01gt1 10757 xrmaxltsup 11261 xrmaxadd 11264 xrbdtri 11279 cvgratz 11535 zdvdsdc 11814 divalglemeunn 11920 divalglemex 11921 divalglemeuneg 11922 divalg 11923 znege1 12172 ennnfonelemk 12395 isxmet2d 13741 trilpolemres 14672 trirec0 14674 |
Copyright terms: Public domain | W3C validator |