theorem pimeq1i {x: nat} (p1 p2 q: wff x): $ p1 <-> p2 $ > $ (P. x p1 -> q) <-> (P. x p2 -> q) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | p1 <-> p2 |
|
2 | 1 | a1i | T. -> (p1 <-> p2) |
3 | 2 | pimeq1d | T. -> ((P. x p1 -> q) <-> (P. x p2 -> q)) |
4 | 3 | trud | (P. x p1 -> q) <-> (P. x p2 -> q) |