![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bi1 | GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
bi1 | ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 110 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 104 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 2 | simpld 105 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimpi 113 bicom1 122 biimpd 132 ibd 167 pm5.74 168 bi3ant 213 pm5.501 233 pm5.32d 423 pm5.19 622 con4biddc 754 con1biimdc 767 bijadc 776 pclem6 1265 albi 1357 exbi 1495 equsexd 1617 cbv2h 1634 sbiedh 1670 eumo0 1931 ceqsalt 2580 vtoclgft 2604 spcgft 2630 pm13.183 2681 reu6 2730 reu3 2731 sbciegft 2793 fv3 5197 prnmaxl 6586 prnminu 6587 elabgft1 9917 elabgf2 9919 bj-axemptylem 10012 bj-notbi 10045 bj-inf2vn 10099 bj-inf2vn2 10100 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |