![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bicomi | GIF version |
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 16-Sep-2013.) |
Ref | Expression |
---|---|
bicomi.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
bicomi | ⊢ (𝜓 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicomi.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | bicom1 130 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpri 132 bitr2i 184 bitr3i 185 bitr4i 186 bitr3id 193 bitr3di 194 syl6bbr 197 bitr4id 198 pm5.41 250 anidm 394 pm4.87 547 anabs1 562 anabs7 564 pm4.76 594 mtbir 661 sylnibr 667 sylnbir 669 xchnxbir 671 xchbinxr 673 nbn 689 pm4.25 748 pm4.56 770 pm4.77 789 pm3.2an3 1161 syl3anbr 1261 3an6 1301 truan 1349 truimfal 1389 nottru 1392 sbid 1748 cleljust 1911 sb10f 1971 necon3bbii 2346 rspc2gv 2805 alexeq 2815 ceqsrexbv 2820 clel2 2822 clel4 2825 dfsbcq2 2916 cbvreucsf 3069 dfdif3 3191 raldifb 3221 difab 3350 un0 3401 in0 3402 ss0b 3407 rexdifpr 3560 iindif2m 3888 epse 4272 abnex 4376 uniuni 4380 elco 4713 cotr 4928 issref 4929 mptpreima 5040 ralrnmpt 5570 rexrnmpt 5571 eroveu 6528 fprodseq 11384 toptopon 12224 xmeterval 12643 txmetcnp 12726 dedekindicclemicc 12818 eldvap 12859 bdeq 13192 bd0r 13194 bdcriota 13252 bj-d0clsepcl 13294 bj-dfom 13302 |
Copyright terms: Public domain | W3C validator |