New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 505 | . 2 |
3 | orbi12i.1 | . . 3 | |
4 | 3 | orbi1i 506 | . 2 |
5 | 2, 4 | bitri 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wo 357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-or 359 |
This theorem is referenced by: pm4.78 565 andir 838 anddi 840 dfbi3 863 4exmid 905 3orbi123i 1141 3or6 1263 cadcoma 1395 neorian 2603 elsymdif 3223 sspsstri 3371 rexun 3443 indi 3501 symdif2 3520 unab 3521 inundif 3628 elimif 3691 dfpr2 3749 ssunsn 3866 ssunpr 3868 sspr 3869 sstp 3870 pwpr 3883 pwtp 3884 unipr 3905 uniun 3910 iunun 4046 iunxun 4047 axprimlem2 4089 axsiprim 4093 axins2prim 4095 axins3prim 4096 pwadjoin 4119 pw1un 4163 dfaddc2 4381 nnsucelrlem1 4424 nndisjeq 4429 ltfinex 4464 ltfintrilem1 4465 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 vfinspss 4551 dfphi2 4569 dfop2lem1 4573 proj1op 4600 proj2op 4601 eqop 4611 brun 4692 setconslem2 4732 setconslem3 4733 setconslem7 4737 dfswap2 4741 dmun 4912 xpeq0 5046 cupex 5816 connexex 5913 enprmaplem4 6079 leconnnc 6218 nmembers1lem3 6270 nncdiv3lem2 6276 nchoicelem16 6304 nchoicelem17 6305 nchoicelem18 6306 |
Copyright terms: Public domain | W3C validator |