New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > imbi12d | Unicode version |
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12d.1 | |
imbi12d.2 |
Ref | Expression |
---|---|
imbi12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12d.1 | . . 3 | |
2 | 1 | imbi1d 308 | . 2 |
3 | imbi12d.2 | . . 3 | |
4 | 3 | imbi2d 307 | . 2 |
5 | 2, 4 | bitrd 244 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
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 |
This theorem is referenced by: nfbidf 1774 drnf1 1969 drnf2 1970 equveli 1988 ax11v2 1992 ax11vALT 2097 ax10-16 2190 ax11eq 2193 ax11el 2194 ax11inda 2200 ax11v2-o 2201 mobid 2238 2mo 2282 2eu6 2289 axext3 2336 ralcom2 2775 cbvralf 2829 cbvraldva2 2839 vtoclgaf 2919 vtocl2gaf 2921 vtocl3gaf 2923 rspct 2948 rspc 2949 ceqex 2969 ralab2 3001 mob2 3016 mob 3018 morex 3020 reu7 3031 reu8 3032 sbcimg 3087 csbhypf 3171 cbvralcsf 3198 dfss2f 3264 sbcss 3660 sneqrg 3874 elintab 3937 intss1 3941 intmin 3946 dfiin2g 4000 preqr2g 4126 ssrelk 4211 eqpw1uni 4330 iota5 4359 nnsucelr 4428 nndisjeq 4429 ltfintri 4466 lenltfin 4469 ssfin 4470 ncfinlower 4483 tfinltfinlem1 4500 evenoddnnnul 4514 evenodddisj 4516 eventfin 4517 oddtfin 4518 nnadjoin 4520 sfintfin 4532 tfinnn 4534 spfinsfincl 4539 vfinspsslem1 4550 vfinspss 4551 copsexg 4607 vtoclr 4816 ssrel 4844 ssopr 4846 tz6.12i 5348 dff13f 5472 f1fveq 5473 fununiq 5517 funsi 5520 oprabid 5550 ov3 5599 caovcan 5628 ov2gf 5711 fvmptf 5722 op1st2nd 5790 fnpprod 5843 clos1conn 5879 trd 5921 frd 5922 extd 5923 symd 5924 trrd 5925 antid 5929 iserd 5942 fundmen 6043 fundmeng 6044 enmap2 6068 enpw 6087 sbthlem2 6204 sbth 6206 taddc 6229 letc 6231 ce2le 6233 nclenn 6249 muc0or 6252 spacind 6287 nchoicelem11 6299 nchoicelem12 6300 nchoicelem17 6305 nchoicelem19 6307 frecxp 6314 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |