New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > biimpi | GIF version |
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
biimpi.1 | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
biimpi | ⊢ (φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpi.1 | . 2 ⊢ (φ ↔ ψ) | |
2 | bi1 178 | . 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: sylbi 187 sylib 188 biimpri 197 mpbi 199 syl5bi 208 syl6ib 217 syl7bi 221 syl8ib 222 bitri 240 pm2.53 362 simplbi 446 simprbi 450 sylanb 458 sylan2b 461 pm3.1 484 orbi2i 505 pm2.32 512 anc2l 538 pm3.37 562 dfbi 610 pm2.76 821 pm5.15 859 pm5.16 860 pm5.75 903 rnlem 931 simp1bi 970 simp2bi 971 simp3bi 972 syl3an1b 1218 syl3an2b 1219 syl3an3b 1220 nic-ax 1438 19.25 1603 sbbii 1653 spvw 1666 hbn1fw 1705 excomim 1742 stdpc5 1798 ax10-16 2190 exmoeu 2246 2mo 2282 eqeq1 2359 eleq2 2414 gencbvex 2901 moeq 3012 euind 3023 reuind 3039 eqsbc3r 3103 ssel 3267 unssd 3439 ssind 3479 n0moeu 3562 ss0 3581 uneqdifeq 3638 ssunsn2 3865 eqsn 3867 snex 4111 pwadjoin 4119 prprc2 4122 opkelimagekg 4271 iotabi 4348 uniabio 4349 iotaint 4352 dfiota4 4372 nnsucelrlem3 4426 nnsucelr 4428 nndisjeq 4429 preaddccan2 4455 ltfintri 4466 ssfin 4470 eqtfinrelk 4486 tfinsuc 4498 phi011lem1 4598 phidisjnn 4615 dmxp 4923 resabs1 4992 resima2 5007 imasn 5018 funun 5146 funcnv3 5157 funimass1 5169 funssxp 5233 f1ocnv 5299 f1o00 5317 fsn2 5434 fconst5 5455 oprabid 5550 eloprabga 5578 op1st2nd 5790 pw1fnf1o 5855 clos1induct 5880 peano4nc 6150 dflec2 6210 ce2le 6233 addccan2nc 6265 nchoice 6308 |
Copyright terms: Public domain | W3C validator |