Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orbi12i | Unicode version |
Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbi12i.1 | |
orbi12i.2 |
Ref | Expression |
---|---|
orbi12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi12i.2 | . . 3 | |
2 | 1 | orbi2i 736 | . 2 |
3 | orbi12i.1 | . . 3 | |
4 | 3 | orbi1i 737 | . 2 |
5 | 2, 4 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: andir 793 anddi 795 3orbi123i 1156 3or6 1286 excxor 1341 19.33b2 1593 sbequilem 1794 sborv 1846 sbor 1905 r19.43 2566 rexun 3226 indi 3293 difindiss 3300 symdifxor 3312 unab 3313 dfpr2 3516 rabrsndc 3561 pwprss 3702 pwtpss 3703 unipr 3720 uniun 3725 iunun 3861 iunxun 3862 brun 3949 pwunss 4175 ordsoexmid 4447 onintexmid 4457 dcextest 4465 opthprc 4560 cnvsom 5052 ftpg 5572 tpostpos 6129 eldju 6921 djur 6922 ltexprlemloc 7383 axpre-ltwlin 7659 axpre-apti 7661 axpre-mulext 7664 axpre-suploc 7678 fz01or 9846 cbvsum 11084 fsum3 11111 gcdsupex 11558 gcdsupcl 11559 |
Copyright terms: Public domain | W3C validator |