Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi12i | GIF version |
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12i.1 | ⊢ (𝜑 ↔ 𝜓) |
imbi12i.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
imbi12i | ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12i.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
2 | 1 | imbi2i 225 | . 2 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃)) |
3 | imbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | imbi1i 237 | . 2 ⊢ ((𝜑 → 𝜃) ↔ (𝜓 → 𝜃)) |
5 | 2, 4 | bitri 183 | 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: stdcn 832 nfbii 1449 sbi2v 1864 sbim 1924 sb8mo 2011 cbvmo 2037 necon4ddc 2378 raleqbii 2445 rmo5 2644 cbvrmo 2651 ss2ab 3160 snsssn 3683 trint 4036 ssextss 4137 ordsoexmid 4472 zfregfr 4483 tfi 4491 peano2 4504 peano5 4507 relop 4684 dmcosseq 4805 cotr 4915 issref 4916 cnvsym 4917 intasym 4918 intirr 4920 codir 4922 qfto 4923 cnvpom 5076 cnvsom 5077 funcnvuni 5187 poxp 6122 infmoti 6908 dfinfre 8707 bezoutlembi 11682 algcvgblem 11719 isprm2 11787 ntreq0 12290 ss1oel2o 13178 |
Copyright terms: Public domain | W3C validator |