Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bibi12d | GIF version |
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
imbi12d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
bibi12d | ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | bibi1d 232 | . 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
3 | imbi12d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 3 | bibi2d 231 | . 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
5 | 2, 4 | bitrd 187 | 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: pm5.32 449 bi2bian9 598 cleqh 2264 abbi 2278 cleqf 2331 cbvreuvw 2695 vtoclb 2778 vtoclbg 2782 ceqsexg 2849 elabgf 2863 reu6 2910 ru 2945 sbcbig 2992 sbcne12g 3058 sbcnestgf 3091 preq12bg 3747 nalset 4106 undifexmid 4166 exmidsssn 4175 exmidsssnc 4176 exmidundif 4179 opthg 4210 opelopabsb 4232 wetriext 4548 opeliunxp2 4738 resieq 4888 elimasng 4966 cbviota 5152 iota2df 5171 fnbrfvb 5521 fvelimab 5536 fmptco 5645 fsng 5652 fressnfv 5666 funfvima3 5712 isorel 5770 isocnv 5773 isocnv2 5774 isotr 5778 ovg 5971 caovcang 5994 caovordg 6000 caovord3d 6003 caovord 6004 opeliunxp2f 6197 dftpos4 6222 ecopovsym 6588 ecopovsymg 6591 xpf1o 6801 nneneq 6814 supmoti 6949 supsnti 6961 isotilem 6962 isoti 6963 ltanqg 7332 ltmnqg 7333 elinp 7406 prnmaxl 7420 prnminu 7421 ltasrg 7702 axpre-ltadd 7818 zextle 9273 zextlt 9274 xlesubadd 9810 rexfiuz 10917 climshft 11231 dvdsext 11778 ltoddhalfle 11815 halfleoddlt 11816 bezoutlemmo 11924 bezoutlemeu 11925 bezoutlemle 11926 bezoutlemsup 11927 dfgcd3 11928 dvdssq 11949 rpexp 12064 pcdvdsb 12230 xmeteq0 12906 comet 13046 dedekindeulemuub 13142 dedekindeulemloc 13144 dedekindicclemuub 13151 dedekindicclemloc 13153 logltb 13342 bj-nalset 13618 bj-d0clsepcl 13648 bj-nn0sucALT 13701 |
Copyright terms: Public domain | W3C validator |