![]() |
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 233 | . 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
3 | imbi12d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 3 | bibi2d 232 | . 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
5 | 2, 4 | bitrd 188 | 1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.32 453 bi2bian9 608 cleqh 2277 abbi 2291 cleqf 2344 cbvreuvw 2709 vtoclb 2794 vtoclbg 2798 ceqsexg 2865 elabgf 2879 reu6 2926 ru 2961 sbcbig 3009 sbcne12g 3075 sbcnestgf 3108 preq12bg 3771 nalset 4130 undifexmid 4190 exmidsssn 4199 exmidsssnc 4200 exmidundif 4203 opthg 4234 opelopabsb 4256 wetriext 4572 opeliunxp2 4762 resieq 4912 elimasng 4991 cbviota 5178 iota2df 5197 fnbrfvb 5551 fvelimab 5567 fmptco 5677 fsng 5684 fressnfv 5698 funfvima3 5744 isorel 5802 isocnv 5805 isocnv2 5806 isotr 5810 ovg 6006 caovcang 6029 caovordg 6035 caovord3d 6038 caovord 6039 opeliunxp2f 6232 dftpos4 6257 ecopovsym 6624 ecopovsymg 6627 xpf1o 6837 nneneq 6850 supmoti 6985 supsnti 6997 isotilem 6998 isoti 6999 ltanqg 7377 ltmnqg 7378 elinp 7451 prnmaxl 7465 prnminu 7466 ltasrg 7747 axpre-ltadd 7863 zextle 9320 zextlt 9321 xlesubadd 9857 rexfiuz 10969 climshft 11283 dvdsext 11831 ltoddhalfle 11868 halfleoddlt 11869 bezoutlemmo 11977 bezoutlemeu 11978 bezoutlemle 11979 bezoutlemsup 11980 dfgcd3 11981 dvdssq 12002 rpexp 12123 pcdvdsb 12289 xmeteq0 13492 comet 13632 dedekindeulemuub 13728 dedekindeulemloc 13730 dedekindicclemuub 13737 dedekindicclemloc 13739 logltb 13928 bj-nalset 14269 bj-d0clsepcl 14299 bj-nn0sucALT 14352 |
Copyright terms: Public domain | W3C validator |