| 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 278 | . 2 ⊢ (𝜑 ↔ 𝜃) |
| 5 | 1, 4 | bitr2i 276 | 1 ⊢ (𝜃 ↔ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: biadan 819 pm4.78 935 xor 1017 cases2 1048 4anpull2 1362 nic-ax 1673 nfnbi 1855 2sb6 2086 2sb5 2278 dfsb7 2279 2sb5rf 2477 2sb6rf 2478 eu6lem 2573 eu6 2574 2mo2 2647 2eu7 2658 2eu8 2659 euae 2660 r2exlem 3143 r3al 3197 risset 3233 ralcom4 3286 rexcom4 3288 moelOLD 3405 rabbi 3467 ralxpxfr2d 3646 reuind 3759 dfss2 3969 undif3 4300 unab 4308 inab 4309 n0el 4364 inssdif0 4374 ssundif 4488 raldifsnb 4796 pwtp 4902 uni0b 4933 iinuni 5098 inuni 5350 reusv2lem4 5401 pwtr 5457 opthprc 5749 xpiundir 5757 xpsspw 5819 relun 5821 inopab 5839 difopab 5840 difopabOLD 5841 ralxpf 5857 dmiun 5924 elidinxp 6062 iresn0n0 6072 inisegn0 6116 rniun 6167 imaco 6271 rnco 6272 mptfnf 6703 fnopabg 6705 dff1o2 6853 brprcneu 6896 brprcneuALT 6897 idref 7166 imaiun 7265 sorpss 7748 opabex3d 7990 opabex3rd 7991 opabex3 7992 ovmptss 8118 frpoins3xpg 8165 frpoins3xp3g 8166 poxp2 8168 poxp3 8175 fnsuppres 8216 sbthfilem 9238 ttrcltr 9756 rankc1 9910 aceq1 10157 dfac10 10178 fin41 10484 axgroth6 10868 genpass 11049 infm3 12227 prime 12699 elixx3g 13400 elfz2 13554 elfzuzb 13558 rpnnen2lem12 16261 divalgb 16441 1nprm 16716 maxprmfct 16746 vdwmc 17016 imasleval 17586 issubm 18816 issubg3 19162 efgrelexlemb 19768 isdomn5 20710 isdomn2 20711 isdomn3 20715 ist1-2 23355 unisngl 23535 elflim2 23972 isfcls 24017 istlm 24193 isnlm 24696 ishl2 25404 ovoliunlem1 25537 eln0s 28358 zaddscl 28380 readdscl 28431 remulscl 28434 erclwwlkref 30039 erclwwlknref 30088 0wlk 30135 h1de2ctlem 31574 nonbooli 31670 5oalem7 31679 ho01i 31847 rnbra 32126 cvnbtwn3 32307 chrelat2i 32384 difrab2 32517 uniinn0 32563 disjex 32605 maprnin 32742 ordtconnlem1 33923 esum2dlem 34093 eulerpartgbij 34374 eulerpartlemr 34376 eulerpartlemn 34383 ballotlem2 34491 bnj976 34791 bnj1185 34807 bnj543 34907 bnj571 34920 bnj611 34932 bnj916 34947 bnj1000 34955 bnj1040 34986 iscvm 35264 untuni 35709 dfso3 35720 dffr5 35754 elima4 35776 brtxpsd3 35897 brbigcup 35899 fixcnv 35909 ellimits 35911 elfuns 35916 brimage 35927 brcart 35933 brimg 35938 brapply 35939 brcup 35940 brcap 35941 dfrdg4 35952 dfint3 35953 ellines 36153 elicc3 36318 bj-snsetex 36964 bj-snglc 36970 bj-projun 36995 wl-2xor 37484 wl-cases2-dnf 37513 poimirlem27 37654 mblfinlem2 37665 iscrngo2 38004 n0elqs 38327 inxpxrn 38396 eqvrelcoss3 38619 prtlem70 38858 prtlem100 38860 prtlem15 38876 prter2 38882 lcvnbtwn3 39029 ishlat1 39353 ishlat2 39354 hlrelat2 39405 islpln5 39537 islvol5 39581 pclclN 39893 cdleme0nex 40292 eu6w 42686 aaitgo 43174 onmaxnelsup 43235 onsupnmax 43240 nnoeomeqom 43325 imaiun1 43664 relexp0eq 43714 ntrk1k3eqk13 44063 2sbc6g 44434 2sbc5g 44435 2reu7 47123 2reu8 47124 mosssn2 48736 alsconv 49309 |
| Copyright terms: Public domain | W3C validator |