![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bicomd | GIF version |
Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bicomd.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
bicomd | ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicomd.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bicom 128 | . 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓)) | |
3 | 1, 2 | sylib 127 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: impbid2 131 syl5ibr 145 ibir 166 bitr2d 178 bitr3d 179 bitr4d 180 syl5rbb 182 syl6rbb 186 pm5.5 231 anabs5 507 con2bidc 769 con1biidc 771 con2biidc 773 pm4.63dc 780 pm4.64dc 801 pm5.55dc 819 baibr 829 baibd 832 rbaibd 833 pm4.55dc 846 anordc 863 pm5.75 869 ninba 879 xor3dc 1278 3impexpbicomi 1328 cbvexh 1638 sbequ12r 1655 sbco 1842 sbcomxyyz 1846 sbal1yz 1877 cbvab 2160 nnedc 2211 necon3bbid 2245 necon2abiidc 2269 necon2bbii 2270 gencbvex 2600 gencbval 2602 sbhypf 2603 clel3g 2678 reu8 2737 sbceq2a 2774 sbcco2 2786 sbcsng 3429 opabid 3994 soeq2 4053 tfisi 4310 posng 4412 xpiindim 4473 fvopab6 5264 fconstfvm 5379 cbvfo 5425 cbvexfo 5426 f1eqcocnv 5431 isoid 5450 isoini 5457 resoprab2 5598 dfoprab3 5817 nnacan 6085 nnmcan 6092 dfmpq2 6453 div4p1lem1div2 8177 ztri3or 8288 nn0ind-raph 8355 zindd 8356 qreccl 8576 iooshf 8821 fzofzim 9044 elfzomelpfzo 9087 frec2uzltd 9189 iiserex 9859 bj-indeq 10053 |
Copyright terms: Public domain | W3C validator |