![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > entri | Structured version Visualization version GIF version |
Description: A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
Ref | Expression |
---|---|
entri.1 | ⊢ 𝐴 ≈ 𝐵 |
entri.2 | ⊢ 𝐵 ≈ 𝐶 |
Ref | Expression |
---|---|
entri | ⊢ 𝐴 ≈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | entri.1 | . 2 ⊢ 𝐴 ≈ 𝐵 | |
2 | entri.2 | . 2 ⊢ 𝐵 ≈ 𝐶 | |
3 | entr 8248 | . 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | |
4 | 1, 2, 3 | mp2an 684 | 1 ⊢ 𝐴 ≈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4844 ≈ cen 8193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2378 ax-ext 2778 ax-sep 4976 ax-nul 4984 ax-pow 5036 ax-pr 5098 ax-un 7184 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2592 df-eu 2610 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3388 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-pw 4352 df-sn 4370 df-pr 4372 df-op 4376 df-uni 4630 df-br 4845 df-opab 4907 df-id 5221 df-xp 5319 df-rel 5320 df-cnv 5321 df-co 5322 df-dm 5323 df-rn 5324 df-res 5325 df-ima 5326 df-fun 6104 df-fn 6105 df-f 6106 df-f1 6107 df-fo 6108 df-f1o 6109 df-er 7983 df-en 8197 |
This theorem is referenced by: entr2i 8251 entr3i 8252 entr4i 8253 infxpenc2 9132 cfpwsdom 9695 hashxplem 13468 xpnnen 15274 qnnen 15277 rpnnen 15291 rexpen 15292 odhash 18301 cygctb 18607 met2ndci 22654 re2ndc 22931 iscmet3 23418 dyadmbl 23707 opnmblALT 23710 mbfimaopnlem 23762 aannenlem3 24425 mblfinlem1 33934 heiborlem3 34098 heibor 34106 irrapx1 38173 zenom 39973 qenom 40316 |
Copyright terms: Public domain | W3C validator |