Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfbi2 | GIF version |
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
dfbi2 | ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 115 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 109 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 1 | simpri 111 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)) |
4 | 2, 3 | impbii 124 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm4.71 381 pm5.17dc 843 dcbi 877 orbididc 894 trubifal 1347 albiim 1416 hbbi 1480 hbbid 1507 nfbid 1520 spsbbi 1765 sbbi 1874 cleqh 2178 ralbiim 2491 reu8 2788 sseq2 3021 soeq2 4071 fun11 4986 dffo3 5335 bdbi 10617 |
Copyright terms: Public domain | W3C validator |