![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baibr | Structured version Visualization version GIF version |
Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.) |
Ref | Expression |
---|---|
baib.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
baibr | ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | baib.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | baib 535 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
3 | 2 | bicomd 222 | 1 ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: rbaibr 537 pm5.44 542 exmoeub 2566 ssnelpss 4103 brinxp 5744 copsex2ga 5797 canth 7354 riotaxfrd 7392 iscard 9966 kmlem14 10154 ltxrlt 11281 elioo5 13378 prmind2 16619 pcelnn 16802 isnirred 20312 isreg2 23203 comppfsc 23358 kqcldsat 23559 elmptrab 23653 itg2uba 25595 prmorcht 27026 adjeq 31657 lnopcnbd 31758 cvexchlem 32090 maprnin 32425 topfne 35729 ismblfin 37019 ftc1anclem5 37055 isdmn2 37413 cdlemefrs29pre00 39756 cdlemefrs29cpre1 39759 isdomn3 42435 elmapintab 42836 bits0ALTV 46832 |
Copyright terms: Public domain | W3C validator |