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 944 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
3 | 2 | bicomd 212 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: cador 1538 reusv1 4792 reusv1OLD 4793 reusv2lem1 4794 opres 5326 cores 5555 fvres 6117 fpwwe2 9344 fzsplit2 12237 saddisjlem 15024 smupval 15048 smueqlem 15050 prmrec 15464 ablnsg 18073 cnprest 20903 flimrest 21597 fclsrest 21638 tsmssubm 21756 setsxms 22094 tchcph 22844 ellimc2 23447 fsumvma2 24739 chpub 24745 mdbr2 28539 mdsl2i 28565 fzsplit3 28940 posrasymb 28988 trleile 28997 cnvcnvintabd 36925 |
Copyright terms: Public domain | W3C validator |