Metamath Proof Explorer

Theorem entr3i

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

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

Proof

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