![]() |
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 536 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
3 | 2 | bicomd 224 | 1 ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → 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: rbaibr 538 pm5.44 543 exmoeub 2625 ssnelpss 4013 brinxp 5521 copsex2ga 5571 canth 6979 riotaxfrd 7013 iscard 9255 kmlem14 9440 ltxrlt 10563 elioo5 12649 prmind2 15863 pcelnn 16040 isnirred 19145 isreg2 21674 comppfsc 21829 kqcldsat 22030 elmptrab 22124 itg2uba 24032 prmorcht 25442 adjeq 29408 lnopcnbd 29509 cvexchlem 29841 maprnin 30160 topfne 33317 ismblfin 34489 ftc1anclem5 34527 isdmn2 34890 cdlemefrs29pre00 37087 cdlemefrs29cpre1 37090 isdomn3 39314 elmapintab 39466 bits0ALTV 43352 |
Copyright terms: Public domain | W3C validator |