theorem cbvpim {x y: nat} (p1 q1: wff x) (p2 q2: wff y):
$ x = y -> (p1 <-> p2) $ >
$ x = y -> (q1 <-> q2) $ >
$ (P. x p1 -> q1) <-> (P. y p2 -> q2) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv | F/ y p1 |
|
| 2 | nfv | F/ y q1 |
|
| 3 | nfv | F/ x p2 |
|
| 4 | nfv | F/ x q2 |
|
| 5 | hyp e1 | x = y -> (p1 <-> p2) |
|
| 6 | hyp e2 | x = y -> (q1 <-> q2) |
|
| 7 | 1, 2, 3, 4, 5, 6 | cbvpimh | (P. x p1 -> q1) <-> (P. y p2 -> q2) |