![]() |
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 226 | . 2 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃)) |
3 | imbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | imbi1i 238 | . 2 ⊢ ((𝜑 → 𝜃) ↔ (𝜓 → 𝜃)) |
5 | 2, 4 | bitri 184 | 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: stdcn 847 nfbii 1473 sbi2v 1892 sbim 1953 sb8mo 2040 cbvmo 2066 necon4ddc 2419 raleqbii 2489 rmo5 2692 cbvrmo 2702 ss2ab 3223 snsssn 3759 trint 4113 ssextss 4217 ordsoexmid 4558 zfregfr 4570 tfi 4578 peano2 4591 peano5 4594 relop 4773 dmcosseq 4894 cotr 5006 issref 5007 cnvsym 5008 intasym 5009 intirr 5011 codir 5013 qfto 5014 cnvpom 5167 cnvsom 5168 funcnvuni 5281 poxp 6227 infmoti 7021 dfinfre 8899 bezoutlembi 11986 algcvgblem 12029 isprm2 12097 ntreq0 13296 ss1oel2o 14396 |
Copyright terms: Public domain | W3C validator |