theorem pimeqd (G: wff) {x: nat} (p1 p2 q1 q2: wff x): $ G -> (p1 <-> p2) $ > $ G -> (q1 <-> q2) $ > $ G -> ((P. x p1 -> q1) <-> (P. x p2 -> q2)) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | G -> (p1 <-> p2) |
|
2 | 1 | pimeq1d | G -> ((P. x p1 -> q1) <-> (P. x p2 -> q1)) |
3 | hyp h2 | G -> (q1 <-> q2) |
|
4 | 3 | pimeq2d | G -> ((P. x p2 -> q1) <-> (P. x p2 -> q2)) |
5 | 2, 4 | bitrd | G -> ((P. x p1 -> q1) <-> (P. x p2 -> q2)) |