Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orbi2d | Unicode version |
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
orbid.1 |
Ref | Expression |
---|---|
orbi2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbid.1 | . . . 4 | |
2 | 1 | biimpd 143 | . . 3 |
3 | 2 | orim2d 777 | . 2 |
4 | 1 | biimprd 157 | . . 3 |
5 | 4 | orim2d 777 | . 2 |
6 | 3, 5 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1d 780 orbi12d 782 dn1dc 944 xorbi2d 1358 eueq2dc 2857 r19.44mv 3457 rexprg 3575 rextpg 3577 exmidsssn 4125 exmidsssnc 4126 swopolem 4227 sowlin 4242 elsucg 4326 elsuc2g 4327 ordsoexmid 4477 poleloe 4938 isosolem 5725 freceq2 6290 brdifun 6456 pitric 7129 elinp 7282 prloc 7299 ltexprlemloc 7415 suplocexprlemloc 7529 ltsosr 7572 aptisr 7587 suplocsrlemb 7614 axpre-ltwlin 7691 axpre-suploclemres 7709 axpre-suploc 7710 gt0add 8335 apreap 8349 apreim 8365 elznn0 9069 elznn 9070 peano2z 9090 zindd 9169 elfzp1 9852 fzm1 9880 fzosplitsni 10012 cjap 10678 dvdslelemd 11541 zeo5 11585 lcmval 11744 lcmneg 11755 lcmass 11766 isprm6 11825 dedekindeulemloc 12766 dedekindeulemeu 12769 suplociccreex 12771 dedekindicclemloc 12775 dedekindicclemeu 12778 bj-nn0sucALT 13176 |
Copyright terms: Public domain | W3C validator |