![]() |
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 536 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
3 | 2 | bicomd 222 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: pm5.75 1026 cador 1601 reusv1 5400 reusv2lem1 5401 fpwwe2 10682 fzsplit2 13575 saddisjlem 16459 smupval 16483 smueqlem 16485 prmrec 16919 ablnsg 19840 cnprest 23276 flimrest 23970 fclsrest 24011 tsmssubm 24130 setsxms 24470 tcphcph 25248 ellimc2 25889 fsumvma2 27235 chpub 27241 mdbr2 32221 mdsl2i 32247 fzsplit3 32685 posrasymb 32823 trleile 32829 fvineqsneu 37066 cnvcnvintabd 43204 grumnud 43897 mofeu 48152 |
Copyright terms: Public domain | W3C validator |