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 202 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | df-an 385 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
3 | 1, 2 | bitr4i 266 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: dfbi 659 pm4.71 660 pm5.17 928 xor 931 albiim 1806 nfbid 1820 nfbidOLD 2230 sbbi 2389 ralbiim 3051 reu8 3369 sseq2 3590 soeq2 4979 fun11 5877 dffo3 6282 isnsg2 17447 isarchi 29067 axextprim 30832 biimpexp 30852 axextndbi 30954 ifpdfbi 36837 ifpidg 36855 ifp1bi 36866 ifpbibib 36874 rp-fakeanorass 36877 frege54cor0a 37177 dffo3f 38359 aibandbiaiffaiffb 39710 aibandbiaiaiffb 39711 |
Copyright terms: Public domain | W3C validator |