| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rbaib | Structured version Visualization version GIF version | ||
| Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
| Ref | Expression |
|---|---|
| baib.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
| Ref | Expression |
|---|---|
| rbaib | ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | baib.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
| 2 | 1 | rbaibr 546 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
| 3 | 2 | bicomd 226 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 |
| 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 210 df-an 401 |
| This theorem is referenced by: pm5.75 1044 cador 1631 reusv1 5359 reusv2lem1 5360 fpwwe2 10616 fzsplit2 13568 saddisjlem 16512 smupval 16536 smueqlem 16538 prmrec 16972 ablnsg 19908 cnprest 23407 flimrest 24101 fclsrest 24142 tsmssubm 24261 setsxms 24597 tcphcph 25357 ellimc2 25997 fsumvma2 27336 chpub 27342 mdbr2 32557 mdsl2i 32583 fzsplit3 33050 posrasymb 33200 trleile 33204 fvineqsneu 37917 cnvcnvintabd 44188 grumnud 44860 mofeu 49477 |
| Copyright terms: Public domain | W3C validator |