![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > 3bitr4g | GIF version |
Description: More general version of 3bitr4i 268. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3bitr4g.1 | ⊢ (φ → (ψ ↔ χ)) |
3bitr4g.2 | ⊢ (θ ↔ ψ) |
3bitr4g.3 | ⊢ (τ ↔ χ) |
Ref | Expression |
---|---|
3bitr4g | ⊢ (φ → (θ ↔ τ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4g.2 | . . 3 ⊢ (θ ↔ ψ) | |
2 | 3bitr4g.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
3 | 1, 2 | syl5bb 248 | . 2 ⊢ (φ → (θ ↔ χ)) |
4 | 3bitr4g.3 | . 2 ⊢ (τ ↔ χ) | |
5 | 3, 4 | syl6bbr 254 | 1 ⊢ (φ → (θ ↔ τ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: bibi1d 310 pm5.32rd 621 orbi2d 682 orbi1d 683 3orbi123d 1251 3anbi123d 1252 nanbi1 1295 nanbi2 1296 xorbi12d 1315 hadbi123d 1382 cadbi123d 1383 cad1 1398 had0 1403 nfbidf 1774 drex1 1967 drnf1 1969 drnf2 1970 cbvexd 2009 drsb1 2022 sbal2 2134 eujustALT 2207 eubid 2211 mobid 2238 eqeq1 2359 eqeq2 2362 eleq1 2413 eleq2 2414 nfceqdf 2488 drnfc1 2505 drnfc2 2506 neeq1 2524 neeq2 2525 neleq1 2607 neleq2 2608 ralbida 2628 rexbida 2629 ralbidv2 2636 rexbidv2 2637 r19.21t 2699 r19.23t 2728 ralcom2 2775 reubida 2793 rmobida 2798 raleqf 2803 rexeqf 2804 reueq1f 2805 rmoeq1f 2806 cbvraldva2 2839 cbvrexdva2 2840 dfsbcq 3048 sbcbid 3099 sbcrext 3119 sbcabel 3123 sbnfc2 3196 elin 3219 elun 3220 psseq1 3356 psseq2 3357 ssconb 3399 uneq1 3411 ineq1 3450 difin2 3516 reuun2 3538 reldisj 3594 undif4 3607 disjssun 3608 pssdifcom1 3635 pssdifcom2 3636 sbcss 3660 eltpg 3769 raltpg 3777 rextpg 3778 intmin4 3955 dfiun2g 3999 iindif2 4035 iinin2 4036 iinxprg 4043 ssofeq 4077 xpkeq1 4198 xpkeq2 4199 opkelimagekg 4271 iotaeq 4347 sniota 4369 sfineq1 4526 sfineq2 4527 phialllem1 4616 breq 4641 breq1 4642 breq2 4643 elimasn 5019 dfco2a 5081 imadif 5171 fneq1 5173 fneq2 5174 feq1 5210 feq2 5211 feq3 5212 fcnvres 5243 f1eq1 5253 f1eq2 5254 f1eq3 5255 foeq1 5265 foeq2 5266 foeq3 5267 f1oeq1 5281 f1oeq2 5282 f1oeq3 5283 fun11iun 5305 dmfco 5381 dffo3 5422 funiunfv 5467 dff13 5471 isoeq1 5482 isoeq2 5483 isoeq3 5484 isoeq4 5485 isoeq5 5486 isomin 5496 mpt2eq123 5661 clos1basesucg 5884 erdmrn 5965 ereldm 5971 ce0nnul 6177 nmembers1lem3 6270 epelcres 6328 |
Copyright terms: Public domain | W3C validator |