| 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 537 | . 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: pm5.75 1031 cador 1608 reusv1 5397 reusv2lem1 5398 fpwwe2 10683 fzsplit2 13589 saddisjlem 16501 smupval 16525 smueqlem 16527 prmrec 16960 ablnsg 19865 cnprest 23297 flimrest 23991 fclsrest 24032 tsmssubm 24151 setsxms 24491 tcphcph 25271 ellimc2 25912 fsumvma2 27258 chpub 27264 mdbr2 32315 mdsl2i 32341 fzsplit3 32795 posrasymb 32955 trleile 32961 fvineqsneu 37412 cnvcnvintabd 43613 grumnud 44305 mofeu 48757 |
| Copyright terms: Public domain | W3C validator |