![]() |
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 535 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
3 | 2 | bicomd 215 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: cador 1723 reusv1 5096 reusv2lem1 5097 opelresgOLD2 5638 fpwwe2 9779 fzsplit2 12658 saddisjlem 15558 smupval 15582 smueqlem 15584 prmrec 15996 ablnsg 18602 cnprest 21463 flimrest 22156 fclsrest 22197 tsmssubm 22315 setsxms 22653 tcphcph 23404 ellimc2 24039 fsumvma2 25351 chpub 25357 mdbr2 29709 mdsl2i 29735 fzsplit3 30099 posrasymb 30201 trleile 30210 cnvcnvintabd 38746 |
Copyright terms: Public domain | W3C validator |