Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orbi1d | Unicode version |
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbid.1 |
Ref | Expression |
---|---|
orbi1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbid.1 | . . 3 | |
2 | 1 | orbi2d 764 | . 2 |
3 | orcom 702 | . 2 | |
4 | orcom 702 | . 2 | |
5 | 2, 3, 4 | 3bitr4g 222 | 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: orbi1 766 orbi12d 767 xorbi1d 1344 eueq2dc 2830 uneq1 3193 r19.45mv 3426 rexprg 3545 rextpg 3547 swopolem 4197 sowlin 4212 onsucelsucexmidlem1 4413 onsucelsucexmid 4415 ordsoexmid 4447 isosolem 5693 acexmidlema 5733 acexmidlemb 5734 acexmidlem2 5739 acexmidlemv 5740 freceq1 6257 exmidaclem 7032 exmidac 7033 elinp 7250 prloc 7267 suplocexprlemloc 7497 ltsosr 7540 suplocsrlemb 7582 axpre-ltwlin 7659 axpre-suploclemres 7677 axpre-suploc 7678 apreap 8316 apreim 8332 sup3exmid 8679 nn01to3 9365 ltxr 9517 fzpr 9812 elfzp12 9834 lcmval 11656 lcmass 11678 isprm6 11737 dedekindeulemloc 12677 dedekindeulemeu 12680 suplociccreex 12682 dedekindicclemloc 12686 dedekindicclemeu 12689 |
Copyright terms: Public domain | W3C validator |