![]() |
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 525 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
3 | 2 | bicomd 213 | 1 ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: pm5.44 532 exmoeu2 2645 ssnelpss 3868 brinxp 5321 copsex2ga 5370 canth 6751 riotaxfrd 6785 iscard 9001 kmlem14 9187 ltxrlt 10310 elioo5 12436 prmind2 15605 pcelnn 15781 isnirred 18908 isreg2 21402 comppfsc 21556 kqcldsat 21757 elmptrab 21851 itg2uba 23730 prmorcht 25125 adjeq 29134 lnopcnbd 29235 cvexchlem 29567 maprnin 29846 topfne 32686 ismblfin 33783 ftc1anclem5 33821 isdmn2 34186 cdlemefrs29pre00 36204 cdlemefrs29cpre1 36207 isdomn3 38308 elmapintab 38428 bits0ALTV 42118 |
Copyright terms: Public domain | W3C validator |