Metamath Proof Explorer


Theorem pjcohcli

Description: Closure of composition of projections. (Contributed by NM, 7-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 GC
pjco.2 HC
Assertion pjcohcli AprojGprojHA

Proof

Step Hyp Ref Expression
1 pjco.1 GC
2 pjco.2 HC
3 1 pjfi projG:
4 2 pjfi projH:
5 3 4 hococli AprojGprojHA