![]() |
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 533 | . 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 1721 reusv1 5099 reusv2lem1 5100 opelresgOLD2 5643 fpwwe2 9787 fzsplit2 12666 saddisjlem 15566 smupval 15590 smueqlem 15592 prmrec 16004 ablnsg 18610 cnprest 21471 flimrest 22164 fclsrest 22205 tsmssubm 22323 setsxms 22661 tcphcph 23412 ellimc2 24047 fsumvma2 25359 chpub 25365 mdbr2 29706 mdsl2i 29732 fzsplit3 30096 posrasymb 30198 trleile 30207 cnvcnvintabd 38742 |
Copyright terms: Public domain | W3C validator |