![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > orbi12d | Unicode version |
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bi12d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bi12d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
orbi12d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi12d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | orbi1d 683 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bi12d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | orbi2d 682 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 244 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-or 359 |
This theorem is referenced by: pm4.39 841 3orbi123d 1251 cadbi123d 1383 eueq3 3011 sbcor 3090 sbcorg 3091 elprg 3750 eltpg 3769 preq12bg 4128 nnc0suc 4412 nndisjeq 4429 lefinlteq 4463 evenodddisjlem1 4515 fununi 5160 funcnvuni 5161 fun11iun 5305 unpreima 5408 clos1basesuc 5882 clos1basesucg 5884 connexrd 5930 connexd 5931 qsdisj 5995 ncdisjeq 6148 nc0le1 6216 leconnnc 6218 muc0or 6252 nchoicelem9 6297 nchoicelem16 6304 nchoicelem17 6305 nchoice 6308 |
Copyright terms: Public domain | W3C validator |