| 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 5358 reusv2lem1 5359 fpwwe2 10616 fzsplit2 13565 saddisjlem 16510 smupval 16534 smueqlem 16536 prmrec 16970 ablnsg 19905 cnprest 23403 flimrest 24097 fclsrest 24138 tsmssubm 24257 setsxms 24593 tcphcph 25353 ellimc2 25993 fsumvma2 27332 chpub 27338 mdbr2 32553 mdsl2i 32579 fzsplit3 33046 posrasymb 33195 trleile 33199 fvineqsneu 37912 cnvcnvintabd 44183 grumnud 44855 mofeu 49478 |
| Copyright terms: Public domain | W3C validator |