Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimp | GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
biimp | ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 116 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 110 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 2 | simpld 111 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpi 119 bicom1 130 biimpd 143 ibd 177 pm5.74 178 bi3ant 223 pm5.501 243 pm5.32d 446 notbi 656 pm5.19 696 con4biddc 843 con1biimdc 859 bijadc 868 pclem6 1356 albi 1448 exbi 1584 equsexd 1709 cbv2h 1728 cbv2w 1730 sbiedh 1767 eumo0 2037 ceqsalt 2738 vtoclgft 2762 spcgft 2789 pm13.183 2850 reu6 2901 reu3 2902 sbciegft 2967 ddifstab 3239 exmidsssnc 4165 fv3 5492 prnmaxl 7409 prnminu 7410 elabgft1 13394 elabgf2 13396 bj-axemptylem 13509 bj-inf2vn 13591 bj-inf2vn2 13592 bj-nn0sucALT 13595 |
Copyright terms: Public domain | W3C validator |