![]() |
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 205 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | df-an 388 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
3 | 1, 2 | bitr4i 270 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: dfbi 468 pm4.71 550 pm5.17 994 xor 997 dfbi3 1030 albiim 1852 nfbid 1865 sbbi 2241 sbbivOLD 2250 sbbiALT 2538 eu6OLDOLD 2593 ralbiim 3124 reu8 3636 sseq2 3883 soeq2 5347 fun11 6261 dffo3 6691 isnsg2 18093 isarchi 30483 axextprim 32453 biimpexp 32472 axextndbi 32576 ifpdfbi 39241 ifpidg 39259 ifp1bi 39270 ifpbibib 39278 rp-fakeanorass 39281 frege54cor0a 39578 dffo3f 40868 aibandbiaiffaiffb 42566 aibandbiaiaiffb 42567 afv2orxorb 42839 |
Copyright terms: Public domain | W3C validator |