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 279 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 277 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 |
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 208 |
This theorem is referenced by: biadan 815 pm4.78 928 xor 1008 cases2 1039 noranOLD 1518 nic-ax 1665 2sb6 2085 2sb5 2273 dfsb7 2276 2sb5rf 2488 2sb6rf 2489 eu6lem 2651 eu6 2652 2mo2 2725 2eu7 2738 2eu8 2739 euae 2740 ralanidOLD 3166 r3al 3199 risset 3264 r2exlem 3299 ralxpxfr2d 3636 reuind 3741 undif3 4262 unab 4267 inab 4268 n0el 4318 inssdif0 4326 ssundif 4429 ralf0 4453 raldifsnb 4721 pwtp 4825 unipr 4843 uni0b 4855 iinuni 5011 reusv2lem4 5292 pwtr 5336 opthprc 5609 xpiundir 5616 xpsspw 5675 relun 5677 inopab 5694 difopab 5695 ralxpf 5710 dmiun 5775 elidinxp 5904 iresn0n0 5916 inisegn0 5954 rniun 5999 imaco 6097 rnco 6098 mptfnf 6476 fnopabg 6478 dff1o2 6613 brprcneu 6655 idref 6900 imaiun 6995 sorpss 7443 opabex3d 7655 opabex3rd 7656 opabex3 7657 ovmptss 7777 fnsuppres 7846 rankc1 9287 aceq1 9531 dfac10 9551 fin41 9854 axgroth6 10238 genpass 10419 infm3 11588 prime 12051 elixx3g 12739 elfz2 12887 elfzuzb 12890 rpnnen2lem12 15566 divalgb 15743 1nprm 16011 maxprmfct 16041 vdwmc 16302 imasleval 16802 issubm 17956 issubg3 18235 efgrelexlemb 18805 ist1-2 21883 unisngl 22063 elflim2 22500 isfcls 22545 istlm 22720 isnlm 23211 ishl2 23900 ovoliunlem1 24030 erclwwlkref 27725 erclwwlknref 27775 0wlk 27822 h1de2ctlem 29259 nonbooli 29355 5oalem7 29364 ho01i 29532 rnbra 29811 cvnbtwn3 29992 chrelat2i 30069 nelbOLD 30159 moel 30179 difrab2 30188 uniinn0 30229 disjex 30270 maprnin 30393 ordtconnlem1 31066 esum2dlem 31250 eulerpartgbij 31529 eulerpartlemr 31531 eulerpartlemn 31538 ballotlem2 31645 bnj976 31948 bnj1185 31964 bnj543 32064 bnj571 32077 bnj611 32089 bnj916 32104 bnj1000 32112 bnj1040 32141 iscvm 32403 untuni 32832 dfso3 32847 dffr5 32886 elima4 32916 brtxpsd3 33254 brbigcup 33256 fixcnv 33266 ellimits 33268 elfuns 33273 brimage 33284 brcart 33290 brimg 33295 brapply 33296 brcup 33297 brcap 33298 dfrdg4 33309 dfint3 33310 ellines 33510 elicc3 33562 bj-snsetex 34172 bj-snglc 34178 bj-projun 34203 bj-vjust 34240 wl-cases2-dnf 34634 poimirlem27 34800 mblfinlem2 34811 iscrngo2 35156 n0elqs 35464 inxpxrn 35523 eqvrelcoss3 35733 prtlem70 35873 prtlem100 35875 prtlem15 35891 prter2 35897 lcvnbtwn3 36044 ishlat1 36368 ishlat2 36369 hlrelat2 36419 islpln5 36551 islvol5 36595 pclclN 36907 cdleme0nex 37306 aaitgo 39640 isdomn3 39682 imaiun1 39874 relexp0eq 39924 ntrk1k3eqk13 40278 2sbc6g 40624 2sbc5g 40625 2reu7 43187 2reu8 43188 alsconv 44819 |
Copyright terms: Public domain | W3C validator |