Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi2i | GIF version |
Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |
Ref | Expression |
---|---|
bi.a | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
imbi2i | ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi.a | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
3 | 2 | pm5.74i 179 | 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: imbi12i 238 anidmdbi 396 nan 687 sbcof2 1803 sblimv 1887 sbhb 1933 sblim 1950 2sb6 1977 sbcom2v 1978 2sb6rf 1983 eu1 2044 moabs 2068 mo3h 2072 moanim 2093 2moswapdc 2109 r2alf 2487 r19.21t 2545 rspc2gv 2846 reu2 2918 reu8 2926 2reuswapdc 2934 2rmorex 2936 dfdif3 3237 ssconb 3260 ssin 3349 reldisj 3466 ssundifim 3498 ralm 3519 unissb 3826 repizf2lem 4147 elirr 4525 en2lp 4538 tfi 4566 ssrel 4699 ssrel2 4701 fncnv 5264 fun11 5265 axcaucvglemres 7861 axpre-suploc 7864 suprzclex 9310 raluz2 9538 supinfneg 9554 infsupneg 9555 infssuzex 11904 bezoutlemmain 11953 isprm2 12071 lmres 13042 limcdifap 13425 |
Copyright terms: Public domain | W3C validator |