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 139 | . 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓)) | |
3 | 1, 2 | sylib 121 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: impbid2 142 syl5ibr 155 ibir 176 bitr2d 188 bitr3d 189 bitr4d 190 bitr2id 192 bitr2di 196 pm5.5 241 anabs5 563 con2bidc 865 con1biidc 867 con2biidc 869 pm4.63dc 876 pm4.64dc 890 pm5.55dc 903 baibr 910 baibd 913 rbaibd 914 pm4.55dc 927 anordc 945 pm5.75 951 ninba 961 xor3dc 1376 3impexpbicomi 1426 cbvexv1 1739 cbvexh 1742 sbequ12r 1759 sbco 1955 sbcomxyyz 1959 sbal1yz 1988 cbvab 2288 nnedc 2339 necon3bbid 2374 necon2abiidc 2398 necon2bbiidc 2399 sbralie 2705 gencbvex 2767 gencbval 2769 sbhypf 2770 clel3g 2855 reu8 2917 sbceq2a 2956 sbcco2 2968 sbcsng 3629 ssdifsn 3698 opabid 4229 soeq2 4288 tfisi 4558 posng 4670 xpiindim 4735 fvopab6 5576 fconstfvm 5697 cbvfo 5747 cbvexfo 5748 f1eqcocnv 5753 isoid 5772 isoini 5780 resoprab2 5930 dfoprab3 6151 cnvoprab 6193 nnacan 6471 nnmcan 6478 isotilem 6962 eqinfti 6976 inflbti 6980 infglbti 6981 djuf1olem 7009 dfmpq2 7287 axsuploc 7962 div4p1lem1div2 9101 ztri3or 9225 nn0ind-raph 9299 zindd 9300 qreccl 9571 elpq 9577 iooshf 9879 fzofzim 10113 elfzomelpfzo 10156 zmodid2 10277 q2submod 10310 modfzo0difsn 10320 frec2uzltd 10328 frec2uzled 10354 prhash2ex 10711 iserex 11266 prodrbdc 11501 reef11 11626 absdvdsb 11735 dvdsabsb 11736 modmulconst 11749 dvdsadd 11761 dvdsabseq 11770 odd2np1 11795 mod2eq0even 11800 oddnn02np1 11802 oddge22np1 11803 evennn02n 11804 evennn2n 11805 zeo5 11810 gcdass 11933 lcmdvds 11990 lcmass 11996 divgcdcoprm0 12012 divgcdcoprmex 12013 1nprm 12025 dvdsnprmd 12036 isevengcd2 12069 m1dvdsndvds 12159 |
Copyright terms: Public domain | W3C validator |