Metamath Proof Explorer


Theorem chjvali

Description: Value of join in CH . (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses chjval.1 AC
chjval.2 BC
Assertion chjvali AB=AB

Proof

Step Hyp Ref Expression
1 chjval.1 AC
2 chjval.2 BC
3 chjval ACBCAB=AB
4 1 2 3 mp2an AB=AB