![]() |
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 117 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 111 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 2 | simpld 112 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biimpi 120 bicom1 131 biimpd 144 ibd 178 pm5.74 179 bi3ant 224 pm5.501 244 pm5.32d 450 notbi 666 pm5.19 706 con4biddc 857 con1biimdc 873 bijadc 882 pclem6 1374 albi 1468 exbi 1604 equsexd 1729 cbv2h 1748 cbv2w 1750 sbiedh 1787 eumo0 2057 ceqsalt 2764 vtoclgft 2788 spcgft 2815 pm13.183 2876 reu6 2927 reu3 2928 sbciegft 2994 ddifstab 3268 exmidsssnc 4204 fv3 5539 prnmaxl 7487 prnminu 7488 elabgft1 14533 elabgf2 14535 bj-axemptylem 14647 bj-inf2vn 14729 bj-inf2vn2 14730 bj-nn0sucALT 14733 |
Copyright terms: Public domain | W3C validator |