| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Deduction form of bound-variable hypothesis builder hbab 1875. |
| Ref | Expression |
|---|---|
| hbabd.1 |
|
| hbabd.2 |
|
| Ref | Expression |
|---|---|
| hbabd |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbabd.1 |
. . . . 5
| |
| 2 | ax-7 1304 |
. . . . 5
| |
| 3 | 1, 2 | syl 12 |
. . . 4
|
| 4 | hbabd.2 |
. . . . 5
| |
| 5 | 4 | 2alimi 1339 |
. . . 4
|
| 6 | hbsb4t 1621 |
. . . 4
| |
| 7 | 3, 5, 6 | 3syl 24 |
. . 3
|
| 8 | ax-16 1580 |
. . 3
| |
| 9 | 7, 8 | pm2.61d2 143 |
. 2
|
| 10 | df-clab 1872 |
. 2
| |
| 11 | 10 | albii 1346 |
. 2
|
| 12 | 9, 10, 11 | 3imtr4g 612 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: hbcsb1g 2567 hbcsbg 2569 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-10 1308 ax-12 1310 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 |
| This theorem depends on definitions: df-bi 164 df-an 242 df-ex 1327 df-sb 1536 df-clab 1872 |