| 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 223 | 1 ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ 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 207 df-an 396 |
| This theorem is referenced by: rbaibr 537 pm5.44 542 exmoeub 2580 ssnelpss 4114 brinxp 5764 copsex2ga 5817 canth 7385 riotaxfrd 7422 iscard 10015 kmlem14 10204 ltxrlt 11331 elioo5 13444 prmind2 16722 pcelnn 16908 isnirred 20420 isdomn3 20715 isreg2 23385 comppfsc 23540 kqcldsat 23741 elmptrab 23835 itg2uba 25778 prmorcht 27221 adjeq 31954 lnopcnbd 32055 cvexchlem 32387 maprnin 32742 topfne 36355 ismblfin 37668 ftc1anclem5 37704 isdmn2 38062 cdlemefrs29pre00 40397 cdlemefrs29cpre1 40400 elmapintab 43609 bits0ALTV 47666 |
| Copyright terms: Public domain | W3C validator |