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 682 sbcof2 1790 sblimv 1874 sbhb 1920 sblim 1937 2sb6 1964 sbcom2v 1965 2sb6rf 1970 eu1 2031 moabs 2055 mo3h 2059 moanim 2080 2moswapdc 2096 r2alf 2474 r19.21t 2532 rspc2gv 2828 reu2 2900 reu8 2908 2reuswapdc 2916 2rmorex 2918 dfdif3 3217 ssconb 3240 ssin 3329 reldisj 3445 ssundifim 3477 ralm 3498 unissb 3803 repizf2lem 4123 elirr 4501 en2lp 4514 tfi 4542 ssrel 4675 ssrel2 4677 fncnv 5237 fun11 5238 axcaucvglemres 7820 axpre-suploc 7823 suprzclex 9263 raluz2 9491 supinfneg 9507 infsupneg 9508 infssuzex 11840 bezoutlemmain 11886 isprm2 11998 lmres 12690 limcdifap 13073 |
Copyright terms: Public domain | W3C validator |