theorem coeq (_F1 _F2 _G1 _G2: set): $ _F1 == _F2 -> _G1 == _G2 -> _F1 o> _G1 == _F2 o> _G2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anl | _F1 == _F2 /\ _G1 == _G2 -> _F1 == _F2 |
|
2 | anr | _F1 == _F2 /\ _G1 == _G2 -> _G1 == _G2 |
|
3 | 1, 2 | coeqd | _F1 == _F2 /\ _G1 == _G2 -> _F1 o> _G1 == _F2 o> _G2 |
4 | 3 | exp | _F1 == _F2 -> _G1 == _G2 -> _F1 o> _G1 == _F2 o> _G2 |