| 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 213 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
| 2 | df-an 396 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
| 3 | 1, 2 | bitr4i 278 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: dfbi 475 pm4.71 557 impimprbi 829 pm5.17 1014 xor 1017 dfbi3 1050 ifpdfbi 1071 albiim 1889 nfbid 1902 sbbi 2308 ralbiim 3113 reu8 3739 dfss2 3969 soeq2 5614 fun11 6640 dffo3 7122 dffo3f 7126 isnsg2 19174 isarchi 33189 axextprim 35701 biimpexp 35717 axextndbi 35805 bj-nnfbit 36753 bj-nnfbid 36754 ifpidg 43504 ifp1bi 43515 ifpbibib 43523 rp-fakeanorass 43526 frege54cor0a 43876 aibandbiaiffaiffb 46906 aibandbiaiaiffb 46907 afv2orxorb 47240 |
| Copyright terms: Public domain | W3C validator |