![]() |
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 595 sylnibr 601 sylnbir 603 xchnxbir 605 xchbinxr 607 nbn 614 pm4.25 674 pm4.77 711 pm4.56 805 pm3.2an3 1082 syl3anbr 1178 3an6 1216 truan 1259 truimfal 1298 nottru 1301 sbid 1654 cleljust 1810 sb10f 1868 necon3bbii 2236 alexeq 2664 ceqsrexbv 2669 clel2 2671 clel4 2674 dfsbcq2 2761 cbvreucsf 2904 raldifb 3077 difab 3200 un0 3245 in0 3246 ss0b 3250 iindif2m 3715 epse 4064 uniuni 4149 cotr 4649 issref 4650 mptpreima 4757 ralrnmpt 5252 rexrnmpt 5253 eroveu 6133 bdeq 9278 bd0r 9280 bdcriota 9338 bj-d0clsepcl 9384 bj-dfom 9392 |
Copyright terms: Public domain | W3C validator |