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 944 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
3 | 2 | bicomd 213 | 1 ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 |
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 386 |
This theorem is referenced by: pm5.44 950 exmoeu2 2497 ssnelpss 3718 brinxp 5181 copsex2ga 5231 canth 6608 riotaxfrd 6642 iscard 8801 kmlem14 8985 ltxrlt 10108 elioo5 12231 prmind2 15398 pcelnn 15574 isnirred 18700 isreg2 21181 comppfsc 21335 kqcldsat 21536 elmptrab 21630 itg2uba 23510 prmorcht 24904 adjeq 28794 lnopcnbd 28895 cvexchlem 29227 maprnin 29506 topfne 32349 ismblfin 33450 ftc1anclem5 33489 isdmn2 33854 cdlemefrs29pre00 35683 cdlemefrs29cpre1 35686 isdomn3 37782 elmapintab 37902 bits0ALTV 41590 |
Copyright terms: Public domain | W3C validator |