New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > bitr3i | Unicode version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3i.1 | |
bitr3i.2 |
Ref | Expression |
---|---|
bitr3i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3i.1 | . . 3 | |
2 | 1 | bicomi 193 | . 2 |
3 | bitr3i.2 | . 2 | |
4 | 2, 3 | bitri 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 |
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 |
This theorem is referenced by: 3bitrri 263 3bitr3i 266 3bitr3ri 267 xchnxbi 299 ianor 474 orordi 516 orordir 517 anandi 801 anandir 802 trunantru 1354 falnanfal 1357 cadan 1392 had0 1403 nic-axALT 1439 sbelx 2124 2mos 2283 2eu6 2289 abeq1i 2461 necon1bbii 2568 r19.41 2763 2ralor 2780 rexcom4a 2879 moeq 3012 euind 3023 2reuswap 3038 2reu5 3044 sbcid 3062 sbcco2 3069 sbc7 3073 sbcie2g 3079 eqsbc3 3085 sbcralt 3118 csbid 3143 cbvralcsf 3198 cbvrabcsf 3201 abss 3335 ssab 3336 difrab 3529 neq0 3560 vdif0 3610 ssunsn2 3865 sspr 3869 sstp 3870 prsspw 3878 disj5 3890 uniintsn 3963 dfpw12 4301 insklem 4304 nnsucelrlem3 4426 ltfinex 4464 dfevenfin2 4512 dfoddfin2 4513 proj1op 4600 proj2op 4601 unopab 4638 brab1 4684 opelssetsn 4760 eliunxp 4821 ralxp 4825 rexxp 4826 opelco 4884 cnvco 4894 dmun 4912 elimapw12 4945 iss 5000 imai 5010 imasn 5018 cotr 5026 cnvsym 5027 intasym 5028 intirr 5029 rninxp 5060 dffun2 5119 dffun3 5120 fin 5246 funimass4 5368 fnressn 5438 fvi 5442 resoprab 5581 ov6g 5600 fmpt2x 5730 braddcfn 5826 fnsex 5832 brpprod 5839 fnfullfunlem1 5856 fvfullfunlem2 5862 clos1induct 5880 transex 5910 connexex 5913 foundex 5914 qsexg 5982 enex 6031 xpassen 6057 enpw1pw 6075 enprmaplem1 6076 ovmuc 6130 ovcelem1 6171 ceex 6174 tcfnex 6244 nmembers1lem1 6268 frecxp 6314 fnfreclem2 6318 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |