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 2658 ssnelpss 4085 brinxp 5623 copsex2ga 5673 canth 7100 riotaxfrd 7137 iscard 9392 kmlem14 9577 ltxrlt 10699 elioo5 12782 prmind2 16017 pcelnn 16194 isnirred 19379 isreg2 21913 comppfsc 22068 kqcldsat 22269 elmptrab 22363 itg2uba 24271 prmorcht 25682 adjeq 29639 lnopcnbd 29740 cvexchlem 30072 maprnin 30393 topfne 33599 ismblfin 34814 ftc1anclem5 34852 isdmn2 35214 cdlemefrs29pre00 37411 cdlemefrs29cpre1 37414 isdomn3 39682 elmapintab 39834 bits0ALTV 43721 |
Copyright terms: Public domain | W3C validator |