![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbcbii | GIF version |
Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.) |
Ref | Expression |
---|---|
sbcbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
sbcbii | ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 9 | . . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓)) |
3 | 2 | sbcbidv 2971 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | mptru 1341 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ⊤wtru 1333 [wsbc 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-sbc 2914 |
This theorem is referenced by: eqsbc3r 2973 sbc3an 2974 sbccomlem 2987 sbccom 2988 sbcabel 2994 csbco 3017 sbcnel12g 3024 sbcne12g 3025 sbccsbg 3036 sbccsb2g 3037 csbnestgf 3057 csbabg 3066 sbcssg 3477 sbcrel 4633 difopab 4680 sbcfung 5155 f1od2 6140 mpoxopovel 6146 bezoutlemnewy 11720 bezoutlemstep 11721 bezoutlemmain 11722 |
Copyright terms: Public domain | W3C validator |