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 214 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | df-an 397 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
3 | 1, 2 | bitr4i 279 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: dfbi 476 pm4.71 558 impimprbi 824 pm5.17 1005 xor 1008 dfbi3 1041 norassOLD 1525 albiim 1881 nfbid 1894 sbbi 2308 sbbivOLD 2318 sbbiALT 2604 ralbiim 3171 reu8 3721 sseq2 3990 soeq2 5488 fun11 6421 dffo3 6860 isnsg2 18246 isarchi 30738 axextprim 32824 biimpexp 32843 axextndbi 32946 bj-nnfbit 33978 bj-nnfbid 33979 ifpdfbi 39717 ifpidg 39735 ifp1bi 39746 ifpbibib 39754 rp-fakeanorass 39757 frege54cor0a 40087 dffo3f 41314 aibandbiaiffaiffb 43007 aibandbiaiaiffb 43008 afv2orxorb 43304 |
Copyright terms: Public domain | W3C validator |