![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfbi2 | Structured version Visualization version GIF version |
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.) |
Ref | Expression |
---|---|
dfbi2 | ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi1 212 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | df-an 395 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
3 | 1, 2 | bitr4i 277 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 |
This theorem is referenced by: dfbi 474 pm4.71 556 impimprbi 827 pm5.17 1009 xor 1012 dfbi3 1047 ifpdfbi 1068 albiim 1884 nfbid 1897 sbbi 2297 ralbiim 3102 reu8 3726 dfss2 3964 sseq2 4005 soeq2 5615 fun11 6632 dffo3 7115 dffo3f 7119 isnsg2 19145 isarchi 33024 axextprim 35471 biimpexp 35487 axextndbi 35576 bj-nnfbit 36405 bj-nnfbid 36406 ifpidg 43095 ifp1bi 43106 ifpbibib 43114 rp-fakeanorass 43117 frege54cor0a 43467 aibandbiaiffaiffb 46446 aibandbiaiaiffb 46447 afv2orxorb 46778 |
Copyright terms: Public domain | W3C validator |