Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi1i | GIF version |
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
Ref | Expression |
---|---|
imbi1i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
imbi1i | ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | imbi1 225 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: imbi12i 228 ancomsimp 1329 sbrim 1830 sbal1yz 1877 sbmo 1959 mo4f 1960 moanim 1974 necon4addc 2275 necon1bddc 2282 nfraldya 2358 r3al 2366 r19.23t 2423 ceqsralt 2581 ralab 2701 ralrab 2702 euind 2728 reu2 2729 rmo4 2734 reuind 2744 rmo3 2849 raldifb 3083 unss 3117 ralunb 3124 inssdif0im 3291 ssundifim 3306 raaan 3327 pwss 3374 ralsnsg 3407 ralsns 3408 disjsn 3432 snss 3494 unissb 3610 intun 3646 intpr 3647 dfiin2g 3690 dftr2 3856 repizf2lem 3914 axpweq 3924 zfpow 3928 axpow2 3929 zfun 4171 uniex2 4173 setindel 4263 setind 4264 elirr 4266 en2lp 4278 zfregfr 4298 tfi 4305 raliunxp 4477 dffun2 4912 dffun4 4913 dffun4f 4918 dffun7 4928 funcnveq 4962 fununi 4967 addnq0mo 6545 mulnq0mo 6546 addsrmo 6828 mulsrmo 6829 prime 8337 raluz2 8522 ralrp 8604 bdcriota 10003 bj-uniex2 10036 bj-ssom 10060 |
Copyright terms: Public domain | W3C validator |