Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbcbii | GIF version |
Description: Formula-building inference rule 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 2872 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | trud 1293 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 ⊤wtru 1285 [wsbc 2815 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-11 1437 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-tru 1287 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-sbc 2816 |
This theorem is referenced by: eqsbc3r 2874 sbc3an 2875 sbccomlem 2888 sbccom 2889 sbcabel 2895 csbco 2917 sbcnel12g 2923 sbcne12g 2924 sbccsbg 2934 sbccsb2g 2935 csbnestgf 2954 csbabg 2963 sbcssg 3350 sbcrel 4444 difopab 4487 sbcfung 4945 f1od2 5876 mpt2xopovel 5879 bezoutlemnewy 10385 bezoutlemstep 10386 bezoutlemmain 10387 |
Copyright terms: Public domain | W3C validator |