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 syl5rbb 192 syl6rbb 196 pm5.5 241 anabs5 562 con2bidc 860 con1biidc 862 con2biidc 864 pm4.63dc 871 pm4.64dc 885 pm5.55dc 898 baibr 905 baibd 908 rbaibd 909 pm4.55dc 922 anordc 940 pm5.75 946 ninba 956 xor3dc 1365 3impexpbicomi 1415 cbvexh 1728 sbequ12r 1745 sbco 1939 sbcomxyyz 1943 sbal1yz 1974 cbvab 2261 nnedc 2311 necon3bbid 2346 necon2abiidc 2370 necon2bbiidc 2371 sbralie 2665 gencbvex 2727 gencbval 2729 sbhypf 2730 clel3g 2814 reu8 2875 sbceq2a 2914 sbcco2 2926 sbcsng 3577 ssdifsn 3646 opabid 4174 soeq2 4233 tfisi 4496 posng 4606 xpiindim 4671 fvopab6 5510 fconstfvm 5631 cbvfo 5679 cbvexfo 5680 f1eqcocnv 5685 isoid 5704 isoini 5712 resoprab2 5861 dfoprab3 6082 cnvoprab 6124 nnacan 6401 nnmcan 6408 isotilem 6886 eqinfti 6900 inflbti 6904 infglbti 6905 djuf1olem 6931 dfmpq2 7156 axsuploc 7830 div4p1lem1div2 8966 ztri3or 9090 nn0ind-raph 9161 zindd 9162 qreccl 9427 iooshf 9728 fzofzim 9958 elfzomelpfzo 10001 zmodid2 10118 q2submod 10151 modfzo0difsn 10161 frec2uzltd 10169 frec2uzled 10195 prhash2ex 10548 iserex 11101 prodrbdc 11336 reef11 11395 absdvdsb 11500 dvdsabsb 11501 modmulconst 11514 dvdsadd 11525 dvdsabseq 11534 odd2np1 11559 mod2eq0even 11564 oddnn02np1 11566 oddge22np1 11567 evennn02n 11568 evennn2n 11569 zeo5 11574 gcdass 11692 lcmdvds 11749 lcmass 11755 divgcdcoprm0 11771 divgcdcoprmex 11772 1nprm 11784 dvdsnprmd 11795 isevengcd2 11825 bj-indeq 13116 |
Copyright terms: Public domain | W3C validator |