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 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 445 notbi 655 pm5.19 695 con4biddc 842 con1biimdc 858 bijadc 867 pclem6 1352 albi 1444 exbi 1583 equsexd 1707 cbv2h 1724 sbiedh 1760 eumo0 2030 ceqsalt 2712 vtoclgft 2736 spcgft 2763 pm13.183 2822 reu6 2873 reu3 2874 sbciegft 2939 ddifstab 3208 exmidsssnc 4126 fv3 5444 prnmaxl 7296 prnminu 7297 elabgft1 12985 elabgf2 12987 bj-axemptylem 13090 bj-inf2vn 13172 bj-inf2vn2 13173 bj-nn0sucALT 13176 |
Copyright terms: Public domain | W3C validator |