![]() |
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 2763 vtoclgft 2787 spcgft 2814 pm13.183 2875 reu6 2926 reu3 2927 sbciegft 2993 ddifstab 3267 exmidsssnc 4203 fv3 5538 prnmaxl 7486 prnminu 7487 elabgft1 14500 elabgf2 14502 bj-axemptylem 14614 bj-inf2vn 14696 bj-inf2vn2 14697 bj-nn0sucALT 14700 |
Copyright terms: Public domain | W3C validator |