Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4g | GIF version |
Description: More general version of 3bitr4i 211. 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 191 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr4g.3 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
5 | 3, 4 | syl6bbr 197 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bibi1d 232 pm5.32rd 446 orbi1d 780 stbid 817 dcbid 823 pm4.14dc 875 orbididc 937 3orbi123d 1289 3anbi123d 1290 xorbi2d 1358 xorbi1d 1359 nfbidf 1519 drnf1 1711 drnf2 1712 drsb1 1771 sbal2 1997 eubidh 2005 eubid 2006 mobidh 2033 mobid 2034 eqeq1 2146 eqeq2 2149 eleq1w 2200 eleq2w 2201 eleq1 2202 eleq2 2203 nfceqdf 2280 drnfc1 2298 drnfc2 2299 neeq1 2321 neeq2 2322 neleq1 2407 neleq2 2408 dfrex2dc 2428 ralbida 2431 rexbida 2432 ralbidv2 2439 rexbidv2 2440 r19.21t 2507 r19.23t 2539 reubida 2612 rmobida 2617 raleqf 2622 rexeqf 2623 reueq1f 2624 rmoeq1f 2625 cbvraldva2 2661 cbvrexdva2 2662 dfsbcq 2911 sbcbi2 2959 sbcbid 2966 eqsbc3r 2969 sbcabel 2990 sbnfc2 3060 ssconb 3209 uneq1 3223 ineq1 3270 difin2 3338 reuun2 3359 reldisj 3414 undif4 3425 disjssun 3426 sbcssg 3472 eltpg 3569 raltpg 3576 rextpg 3577 r19.12sn 3589 opeq1 3705 opeq2 3706 intmin4 3799 dfiun2g 3845 iindif2m 3880 iinin2m 3881 breq 3931 breq1 3932 breq2 3933 treq 4032 opthg2 4161 poeq1 4221 soeq1 4237 frforeq1 4265 freq1 4266 frforeq2 4267 freq2 4268 frforeq3 4269 weeq1 4278 weeq2 4279 ordeq 4294 limeq 4299 rabxfrd 4390 iunpw 4401 opthprc 4590 releq 4621 sbcrel 4625 eqrel 4628 eqrelrel 4640 xpiindim 4676 brcnvg 4720 brresg 4827 resieq 4829 xpcanm 4978 xpcan2m 4979 dmsnopg 5010 dfco2a 5039 cnvpom 5081 cnvsom 5082 iotaeq 5096 sniota 5115 sbcfung 5147 fneq1 5211 fneq2 5212 feq1 5255 feq2 5256 feq3 5257 sbcfng 5270 sbcfg 5271 f1eq1 5323 f1eq2 5324 f1eq3 5325 foeq1 5341 foeq2 5342 foeq3 5343 f1oeq1 5356 f1oeq2 5357 f1oeq3 5358 fun11iun 5388 mpteqb 5511 dffo3 5567 fmptco 5586 dff13 5669 f1imaeq 5676 f1eqcocnv 5692 fliftcnv 5696 isoeq1 5702 isoeq2 5703 isoeq3 5704 isoeq4 5705 isoeq5 5706 isocnv2 5713 acexmid 5773 fnotovb 5814 mpoeq123 5830 ottposg 6152 dmtpos 6153 smoeq 6187 nnacan 6408 nnmcan 6415 ereq1 6436 ereq2 6437 elecg 6467 ereldm 6472 ixpiinm 6618 enfi 6767 elfi2 6860 fipwssg 6867 ctssdccl 6996 creur 8717 eqreznegel 9406 ltxr 9562 icoshftf1o 9774 elfzm11 9871 elfzomelpfzo 10008 nn0ennn 10206 nnesq 10411 rexfiuz 10761 cau4 10888 sumeq2 11128 fisumcom2 11207 dvdsflip 11549 divgcdcoprm0 11782 hashdvds 11897 tpspropd 12203 tgss2 12248 lmbr2 12383 txcnmpt 12442 txhmeo 12488 blininf 12593 blres 12603 xmeterval 12604 xmspropd 12646 mspropd 12647 metequiv 12664 xmetxpbl 12677 limcdifap 12800 cbvrald 12995 |
Copyright terms: Public domain | W3C validator |