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 syl5bbr 193 syl5rbbr 194 syl6bbr 197 syl6rbbr 198 pm5.41 250 anidm 393 pm4.87 546 anabs1 561 anabs7 563 pm4.76 593 mtbir 660 sylnibr 666 sylnbir 668 xchnxbir 670 xchbinxr 672 nbn 688 pm4.25 747 pm4.56 769 pm4.77 788 pm3.2an3 1160 syl3anbr 1260 3an6 1300 truan 1348 truimfal 1388 nottru 1391 sbid 1747 cleljust 1908 sb10f 1968 necon3bbii 2343 rspc2gv 2796 alexeq 2806 ceqsrexbv 2811 clel2 2813 clel4 2816 dfsbcq2 2907 cbvreucsf 3059 dfdif3 3181 raldifb 3211 difab 3340 un0 3391 in0 3392 ss0b 3397 iindif2m 3875 epse 4259 abnex 4363 uniuni 4367 elco 4700 cotr 4915 issref 4916 mptpreima 5027 ralrnmpt 5555 rexrnmpt 5556 eroveu 6513 toptopon 12174 xmeterval 12593 txmetcnp 12676 dedekindicclemicc 12768 eldvap 12809 bdeq 13010 bd0r 13012 bdcriota 13070 bj-d0clsepcl 13112 bj-dfom 13120 |
Copyright terms: Public domain | W3C validator |