![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4ri | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
Ref | Expression |
---|---|
3bitr4i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr4i.2 | ⊢ (𝜒 ↔ 𝜑) |
3bitr4i.3 | ⊢ (𝜃 ↔ 𝜓) |
Ref | Expression |
---|---|
3bitr4ri | ⊢ (𝜃 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 | . 2 ⊢ (𝜒 ↔ 𝜑) | |
2 | 3bitr4i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitr4i.3 | . . 3 ⊢ (𝜃 ↔ 𝜓) | |
4 | 2, 3 | bitr4i 277 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 275 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 |
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 206 |
This theorem is referenced by: biadan 817 pm4.78 932 xor 1012 cases2 1045 nic-ax 1667 nfnbi 1849 2sb6 2081 2sb5 2266 dfsb7 2268 2sb5rf 2465 2sb6rf 2466 eu6lem 2561 eu6 2562 2mo2 2635 2eu7 2646 2eu8 2647 euae 2648 r2exlem 3132 r3al 3186 risset 3220 ralcom4 3273 rexcom4 3275 moelOLD 3388 rabbi 3449 ralxpxfr2d 3629 reuind 3745 dfss2 3962 undif3 4289 unab 4297 inab 4298 n0el 4361 inssdif0 4371 ssundif 4489 ralf0OLD 4519 raldifsnb 4801 pwtp 4904 uniprOLD 4927 uni0b 4937 iinuni 5102 inuni 5346 reusv2lem4 5401 pwtr 5454 opthprc 5742 xpiundir 5749 xpsspw 5811 relun 5813 inopab 5831 difopab 5832 difopabOLD 5833 ralxpf 5849 dmiun 5916 elidinxp 6048 iresn0n0 6058 inisegn0 6103 rniun 6154 imaco 6257 rnco 6258 mptfnf 6691 fnopabg 6693 dff1o2 6843 brprcneu 6886 brprcneuALT 6887 idref 7155 imaiun 7255 sorpss 7734 opabex3d 7970 opabex3rd 7971 opabex3 7972 ovmptss 8098 frpoins3xpg 8145 frpoins3xp3g 8146 poxp2 8148 poxp3 8155 fnsuppres 8196 sbthfilem 9226 ttrcltr 9741 rankc1 9895 aceq1 10142 dfac10 10162 fin41 10469 axgroth6 10853 genpass 11034 infm3 12206 prime 12676 elixx3g 13372 elfz2 13526 elfzuzb 13530 rpnnen2lem12 16205 divalgb 16384 1nprm 16653 maxprmfct 16683 vdwmc 16950 imasleval 17526 issubm 18763 issubg3 19107 efgrelexlemb 19717 isdomn3 21265 isdomn5 21266 ist1-2 23295 unisngl 23475 elflim2 23912 isfcls 23957 istlm 24133 isnlm 24636 ishl2 25342 ovoliunlem1 25475 eln0s 28273 readdscl 28299 remulscl 28302 erclwwlkref 29902 erclwwlknref 29951 0wlk 29998 h1de2ctlem 31437 nonbooli 31533 5oalem7 31542 ho01i 31710 rnbra 31989 cvnbtwn3 32170 chrelat2i 32247 difrab2 32374 uniinn0 32420 disjex 32461 maprnin 32595 ordtconnlem1 33656 esum2dlem 33842 eulerpartgbij 34123 eulerpartlemr 34125 eulerpartlemn 34132 ballotlem2 34239 bnj976 34539 bnj1185 34555 bnj543 34655 bnj571 34668 bnj611 34680 bnj916 34695 bnj1000 34703 bnj1040 34734 iscvm 35000 untuni 35434 dfso3 35445 dffr5 35479 elima4 35502 brtxpsd3 35623 brbigcup 35625 fixcnv 35635 ellimits 35637 elfuns 35642 brimage 35653 brcart 35659 brimg 35664 brapply 35665 brcup 35666 brcap 35667 dfrdg4 35678 dfint3 35679 ellines 35879 elicc3 35932 bj-snsetex 36573 bj-snglc 36579 bj-projun 36604 wl-2xor 37093 wl-cases2-dnf 37110 poimirlem27 37251 mblfinlem2 37262 iscrngo2 37601 n0elqs 37928 inxpxrn 37997 eqvrelcoss3 38220 prtlem70 38459 prtlem100 38461 prtlem15 38477 prter2 38483 lcvnbtwn3 38630 ishlat1 38954 ishlat2 38955 hlrelat2 39006 islpln5 39138 islvol5 39182 pclclN 39494 cdleme0nex 39893 eu6w 42236 aaitgo 42728 onmaxnelsup 42793 onsupnmax 42798 nnoeomeqom 42883 imaiun1 43223 relexp0eq 43273 ntrk1k3eqk13 43622 2sbc6g 43994 2sbc5g 43995 2reu7 46629 2reu8 46630 mosssn2 48073 iscnrm3lem3 48140 alsconv 48409 |
Copyright terms: Public domain | W3C validator |