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 762 | . 2 |
4 | 1 | biimprd 157 | . . 3 |
5 | 4 | orim2d 762 | . 2 |
6 | 3, 5 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wo 682 |
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 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1d 765 orbi12d 767 dn1dc 929 xorbi2d 1343 eueq2dc 2830 r19.44mv 3427 rexprg 3545 rextpg 3547 exmidsssn 4095 exmidsssnc 4096 swopolem 4197 sowlin 4212 elsucg 4296 elsuc2g 4297 ordsoexmid 4447 poleloe 4908 isosolem 5693 freceq2 6258 brdifun 6424 pitric 7097 elinp 7250 prloc 7267 ltexprlemloc 7383 suplocexprlemloc 7497 ltsosr 7540 aptisr 7555 suplocsrlemb 7582 axpre-ltwlin 7659 axpre-suploclemres 7677 axpre-suploc 7678 gt0add 8302 apreap 8316 apreim 8332 elznn0 9027 elznn 9028 peano2z 9048 zindd 9127 elfzp1 9807 fzm1 9835 fzosplitsni 9967 cjap 10633 dvdslelemd 11453 zeo5 11497 lcmval 11656 lcmneg 11667 lcmass 11678 isprm6 11737 dedekindeulemloc 12677 dedekindeulemeu 12680 suplociccreex 12682 dedekindicclemloc 12686 dedekindicclemeu 12689 bj-nn0sucALT 13072 |
Copyright terms: Public domain | W3C validator |