Metamath Proof Explorer

Theorem entr2i

Description: A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004)

Ref Expression
Hypotheses entr2i.1 
|- A ~~ B
entr2i.2 
|- B ~~ C
Assertion entr2i 
|- C ~~ A

Proof

Step Hyp Ref Expression
1 entr2i.1 
 |-  A ~~ B
2 entr2i.2 
 |-  B ~~ C
3 1 2 entri 
 |-  A ~~ C
4 3 ensymi 
 |-  C ~~ A