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 122 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝜓 ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ 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: biimpri 124 bitr2i 174 bitr3i 175 bitr4i 176 syl5bbr 183 syl5rbbr 184 syl6bbr 187 syl6rbbr 188 pm5.41 240 anidm 376 pm4.87 493 anabs1 506 anabs7 508 pm4.76 536 mtbir 596 sylnibr 602 sylnbir 604 xchnxbir 606 xchbinxr 608 nbn 615 pm4.25 675 pm4.77 712 pm4.56 806 pm3.2an3 1083 syl3anbr 1179 3an6 1217 truan 1260 truimfal 1301 nottru 1304 sbid 1657 cleljust 1813 sb10f 1871 necon3bbii 2242 alexeq 2670 ceqsrexbv 2675 clel2 2677 clel4 2680 dfsbcq2 2767 cbvreucsf 2910 raldifb 3083 difab 3206 un0 3251 in0 3252 ss0b 3256 iindif2m 3724 epse 4079 uniuni 4183 cotr 4706 issref 4707 mptpreima 4814 ralrnmpt 5309 rexrnmpt 5310 eroveu 6197 bdeq 9943 bd0r 9945 bdcriota 10003 bj-d0clsepcl 10049 bj-dfom 10057 |
Copyright terms: Public domain | W3C validator |