Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpjaodan | Unicode version |
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
jaodan.1 | |
jaodan.2 | |
jaodan.3 |
Ref | Expression |
---|---|
mpjaodan |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaodan.3 | . 2 | |
2 | jaodan.1 | . . 3 | |
3 | jaodan.2 | . . 3 | |
4 | 2, 3 | jaodan 710 | . 2 |
5 | 1, 4 | mpdan 398 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: mpjao3dan 1202 ifcldcd 3358 ordtri2or2exmidlem 4251 reg2exmidlema 4259 nndifsnid 6080 phpm 6327 fidifsnen 6331 fidifsnid 6332 fin0 6342 fientri3 6353 mullocprlem 6668 recexprlemloc 6729 z2ge 8739 fztri3or 8903 fzm1 8962 fzneuz 8963 qbtwnzlemstep 9103 rebtwn2zlemstep 9107 expaddzaplem 9298 expnbnd 9372 resqrexlemnm 9616 resqrexlemcvg 9617 resqrexlemoverl 9619 resqrexlemglsq 9620 leabs 9672 nn0abscl 9681 ltabs 9683 abslt 9684 fzomaxdif 9709 nn0seqcvgd 9880 |
Copyright terms: Public domain | W3C validator |