theorem pimeq1d (G: wff) {x: nat} (p1 p2 q: wff x): $ G -> (p1 <-> p2) $ > $ G -> ((P. x p1 -> q) <-> (P. x p2 -> q)) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pimeq1 | A. x (p1 <-> p2) -> ((P. x p1 -> q) <-> (P. x p2 -> q)) |
|
2 | hyp h1 | G -> (p1 <-> p2) |
|
3 | 2 | iald | G -> A. x (p1 <-> p2) |
4 | 1, 3 | syl | G -> ((P. x p1 -> q) <-> (P. x p2 -> q)) |