![]() |
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 267 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 265 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
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 197 |
This theorem is referenced by: pm4.78 605 xor 953 cases2 1016 nannan 1491 nic-ax 1638 2sb5 2471 2sb6 2472 2sb5rf 2479 moabs 2530 2mo2 2579 2eu7 2588 2eu8 2589 r3al 2969 r2exlem 3088 risset 3091 r19.35 3113 ralxpxfr2d 3358 reuind 3444 undif3 3921 undif3OLD 3922 unab 3927 inab 3928 n0el 3973 inssdif0 3980 ssundif 4085 ralf0 4111 raldifsnb 4358 pwtp 4463 unipr 4481 uni0b 4495 iinuni 4641 reusv2lem4 4902 pwtr 4951 elxp2OLD 5167 opthprc 5201 xpiundir 5208 xpsspw 5266 relun 5268 inopab 5285 difopab 5286 ralxpf 5301 dmiun 5365 inisegn0 5532 rniun 5578 imaco 5678 mptfnf 6053 fnopabg 6055 dff1o2 6180 brprcneu 6222 idref 6539 imaiun 6543 sorpss 6984 opabex3d 7187 opabex3 7188 ovmptss 7303 fnsuppres 7367 rankc1 8771 aceq1 8978 dfac10 8997 fin41 9304 axgroth6 9688 genpass 9869 infm3 11020 prime 11496 elixx3g 12226 elfz2 12371 elfzuzb 12374 rpnnen2lem12 14998 divalgb 15174 1nprm 15439 maxprmfct 15468 vdwmc 15729 imasleval 16248 issubm 17394 issubg3 17659 efgrelexlemb 18209 ist1-2 21199 unisngl 21378 elflim2 21815 isfcls 21860 istlm 22035 isnlm 22526 ishl2 23212 erclwwlkref 26977 erclwwlknref 27033 0wlk 27094 h1de2ctlem 28542 nonbooli 28638 5oalem7 28647 ho01i 28815 rnbra 29094 cvnbtwn3 29275 chrelat2i 29352 moel 29451 difrab2 29465 uniinn0 29492 disjex 29531 maprnin 29634 ordtconnlem1 30098 esum2dlem 30282 eulerpartgbij 30562 eulerpartlemr 30564 eulerpartlemn 30571 ballotlem2 30678 bnj976 30974 bnj1185 30990 bnj543 31089 bnj571 31102 bnj611 31114 bnj916 31129 bnj1000 31137 bnj1040 31166 iscvm 31367 untuni 31712 dfso3 31727 dffr5 31769 elima4 31803 brtxpsd3 32128 brbigcup 32130 fixcnv 32140 ellimits 32142 elfuns 32147 brimage 32158 brcart 32164 brimg 32169 brapply 32170 brcup 32171 brcap 32172 dfrdg4 32183 dfint3 32184 ellines 32384 elicc3 32436 bj-ssb1 32758 bj-snsetex 33076 bj-snglc 33082 bj-projun 33107 bj-vjust2 33140 wl-cases2-dnf 33425 poimirlem27 33566 mblfinlem2 33577 iscrngo2 33926 ralanid 34152 n0elqs 34239 inxpxrn 34293 prtlem70 34460 prtlem100 34463 prtlem15 34479 prter2 34485 lcvnbtwn3 34633 ishlat1 34957 ishlat2 34958 hlrelat2 35007 islpln5 35139 islvol5 35183 pclclN 35495 cdleme0nex 35895 aaitgo 38049 isdomn3 38099 imaiun1 38260 relexp0eq 38310 ntrk1k3eqk13 38665 2sbc6g 38933 2sbc5g 38934 2reu7 41512 2reu8 41513 alsconv 42864 |
Copyright terms: Public domain | W3C validator |