theorem oreqd (_G _a1 _a2 _b1 _b2: wff): $ _G -> (_a1 <-> _a2) $ > $ _G -> (_b1 <-> _b2) $ > $ _G -> (_a1 \/ _b1 <-> _a2 \/ _b2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _ah | _G -> (_a1 <-> _a2) |
|
2 | 1 | noteqd | _G -> (~_a1 <-> ~_a2) |
3 | hyp _bh | _G -> (_b1 <-> _b2) |
|
4 | 2, 3 | imeqd | _G -> (~_a1 -> _b1 <-> ~_a2 -> _b2) |
5 | 4 | conv or | _G -> (_a1 \/ _b1 <-> _a2 \/ _b2) |