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 448 bi2bian9 582 cleqh 2217 abbi 2231 cleqf 2282 vtoclb 2717 vtoclbg 2721 ceqsexg 2787 elabgf 2800 reu6 2846 ru 2881 sbcbig 2927 sbcne12g 2991 sbcnestgf 3021 preq12bg 3670 nalset 4028 undifexmid 4087 exmidsssn 4095 exmidsssnc 4096 exmidundif 4099 opthg 4130 opelopabsb 4152 wetriext 4461 opeliunxp2 4649 resieq 4799 elimasng 4877 cbviota 5063 iota2df 5082 fnbrfvb 5430 fvelimab 5445 fmptco 5554 fsng 5561 fressnfv 5575 funfvima3 5619 isorel 5677 isocnv 5680 isocnv2 5681 isotr 5685 ovg 5877 caovcang 5900 caovordg 5906 caovord3d 5909 caovord 5910 opeliunxp2f 6103 dftpos4 6128 ecopovsym 6493 ecopovsymg 6496 xpf1o 6706 nneneq 6719 supmoti 6848 supsnti 6860 isotilem 6861 isoti 6862 ltanqg 7176 ltmnqg 7177 elinp 7250 prnmaxl 7264 prnminu 7265 ltasrg 7546 axpre-ltadd 7662 zextle 9110 zextlt 9111 xlesubadd 9634 rexfiuz 10729 climshft 11041 dvdsext 11480 ltoddhalfle 11517 halfleoddlt 11518 bezoutlemmo 11621 bezoutlemeu 11622 bezoutlemle 11623 bezoutlemsup 11624 dfgcd3 11625 dvdssq 11646 rpexp 11758 xmeteq0 12455 comet 12595 dedekindeulemuub 12691 dedekindeulemloc 12693 dedekindicclemuub 12700 dedekindicclemloc 12702 bj-nalset 13020 bj-d0clsepcl 13050 bj-nn0sucALT 13103 |
Copyright terms: Public domain | W3C validator |