New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 313 | . 2 ⊢ ((φ ↔ ψ) → ((φ → χ) ↔ (ψ → χ))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ((φ → χ) ↔ (ψ → χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: imbi12i 316 imor 401 ancomsimp 1369 19.43 1605 19.37 1873 dfsb3 2056 sbor 2066 sbrim 2067 mo4f 2236 2mos 2283 neor 2600 r3al 2671 r19.23t 2728 r19.43 2766 ceqsralt 2882 ralab 2997 ralrab 2998 euind 3023 reu2 3024 rmo4 3029 reuind 3039 2reu5lem3 3043 rmo3 3133 unss 3437 ralunb 3444 inssdif0 3617 ssundif 3633 dfif2 3664 pwss 3736 ralsns 3763 disjsn 3786 snss 3838 unissb 3921 intun 3958 intpr 3959 dfiin2g 4000 eqpw1 4162 pw111 4170 ssrelk 4211 eqrelk 4212 elp6 4263 sikexlem 4295 insklem 4304 peano5 4409 ltfintrilem1 4465 evenodddisjlem1 4515 nnadjoin 4520 nnpweq 4523 raliunxp 4823 intirr 5029 dffun4 5121 dffun5 5122 dffun7 5133 fun11 5159 fununi 5160 dff13 5471 clos1induct 5880 dfnnc3 5885 enmap2lem4 6066 enmap1lem4 6072 spacind 6287 |
Copyright terms: Public domain | W3C validator |